chore: try to use fast_instance in basic definitions

[sgouezel]

---

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[github-actions]

PR summary df818bb9eb

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.Basic	109	110	+1 (+0.92%)
Mathlib.Data.SetLike.Basic	174	175	+1 (+0.57%)

Import changes for all files

Files

Import difference

251 files Mathlib.Algebra.BigOperators.Group.List.Basic Mathlib.Algebra.BigOperators.Group.List.Lemmas Mathlib.Algebra.EuclideanDomain.Defs Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Group.Action.End Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Conj Mathlib.Algebra.Group.End Mathlib.Algebra.GroupWithZero.Action.Basic Mathlib.Algebra.GroupWithZero.Associated Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.GroupWithZero.Conj Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.BigOperators.Group.List Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.End Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Defs Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Group.End Mathlib.Algebra.Order.Group.Equiv Mathlib.Algebra.Order.Group.Int Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Synonym Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Group.Units Mathlib.Algebra.Order.GroupWithZero.Action.Synonym Mathlib.Algebra.Order.GroupWithZero.Synonym Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs Mathlib.Algebra.Order.Hom.Basic Mathlib.Algebra.Order.Hom.Monoid Mathlib.Algebra.Order.Hom.TypeTags Mathlib.Algebra.Order.Hom.Units Mathlib.Algebra.Order.Module.Synonym Mathlib.Algebra.Order.Monoid.Associated Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Units Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.Units Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Ring.Idempotent Mathlib.Algebra.Order.Ring.Synonym Mathlib.Algebra.Order.Ring.Unbundled.Rat Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Order.Sum Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.Prime.Lemmas Mathlib.Algebra.Ring.Centralizer Mathlib.Algebra.Tropical.Basic Mathlib.AlgebraicTopology.DoldKan.Compatibility Mathlib.CategoryTheory.Bicategory.End Mathlib.CategoryTheory.Bicategory.EqToHom Mathlib.CategoryTheory.Bicategory.Functor.Prelax Mathlib.CategoryTheory.Bicategory.LocallyDiscrete Mathlib.CategoryTheory.Bicategory.Opposites Mathlib.CategoryTheory.Bicategory.Strict.Basic Mathlib.CategoryTheory.Bicategory.Strict Mathlib.CategoryTheory.CatCommSq Mathlib.CategoryTheory.Category.Preorder Mathlib.CategoryTheory.Category.ULift Mathlib.CategoryTheory.CommSq Mathlib.CategoryTheory.Comma.Arrow Mathlib.CategoryTheory.Comma.Basic Mathlib.CategoryTheory.ConcreteCategory.Basic Mathlib.CategoryTheory.DinatTrans Mathlib.CategoryTheory.Discrete.Basic Mathlib.CategoryTheory.Discrete.SumsProducts Mathlib.CategoryTheory.EqToHom Mathlib.CategoryTheory.Equivalence Mathlib.CategoryTheory.EssentialImage Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.CategoryTheory.FiberedCategory.Cartesian Mathlib.CategoryTheory.FiberedCategory.Cocartesian Mathlib.CategoryTheory.FiberedCategory.Fiber Mathlib.CategoryTheory.FiberedCategory.Fibered Mathlib.CategoryTheory.FiberedCategory.HasFibers Mathlib.CategoryTheory.FiberedCategory.HomLift Mathlib.CategoryTheory.Functor.Const Mathlib.CategoryTheory.Functor.CurryingThree Mathlib.CategoryTheory.Functor.Currying Mathlib.CategoryTheory.Functor.OfSequence Mathlib.CategoryTheory.Functor.TwoSquare Mathlib.CategoryTheory.Join.Basic Mathlib.CategoryTheory.Join.Opposites Mathlib.CategoryTheory.Join.Sum Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform Mathlib.CategoryTheory.Monoidal.Action.Basic Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor Mathlib.CategoryTheory.Monoidal.Category Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.ObjectProperty.Basic Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms Mathlib.CategoryTheory.ObjectProperty.Equivalence Mathlib.CategoryTheory.ObjectProperty.FullSubcategory Mathlib.CategoryTheory.ObjectProperty.Opposite Mathlib.CategoryTheory.Opposites Mathlib.CategoryTheory.PEmpty Mathlib.CategoryTheory.PUnit Mathlib.CategoryTheory.Pi.Basic Mathlib.CategoryTheory.Products.Associator Mathlib.CategoryTheory.Products.Basic Mathlib.CategoryTheory.Products.Bifunctor Mathlib.CategoryTheory.Products.Unitor Mathlib.CategoryTheory.Square Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic Mathlib.CategoryTheory.Sums.Products Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Path.Vertices Mathlib.Computability.Tape Mathlib.Computability.TuringMachine.Tape Mathlib.Control.Fix Mathlib.Data.Bool.Set Mathlib.Data.Bundle Mathlib.Data.Fin.Basic Mathlib.Data.FunLike.Graded Mathlib.Data.Int.GCD Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.Range Mathlib.Data.List.Chain Mathlib.Data.List.Destutter Mathlib.Data.List.DropRight Mathlib.Data.List.Infix Mathlib.Data.List.Intervals Mathlib.Data.List.Iterate Mathlib.Data.List.Lex Mathlib.Data.List.MinMax Mathlib.Data.List.Permutation Mathlib.Data.List.Prime Mathlib.Data.List.Range Mathlib.Data.List.Rotate Mathlib.Data.List.SplitBy Mathlib.Data.List.SplitLengths Mathlib.Data.List.Sublists Mathlib.Data.List.TakeWhile Mathlib.Data.Multiset.AddSub Mathlib.Data.Multiset.Basic Mathlib.Data.Multiset.Count Mathlib.Data.Multiset.Defs Mathlib.Data.Multiset.Pairwise Mathlib.Data.Multiset.Replicate Mathlib.Data.Multiset.ZeroCons Mathlib.Data.Nat.Cast.Synonym Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.Choose.Basic Mathlib.Data.Nat.GCD.Prime Mathlib.Data.Nat.Log Mathlib.Data.Nat.Order.Lemmas Mathlib.Data.Nat.Prime.Defs Mathlib.Data.Nat.Upto Mathlib.Data.Nat.WithBot Mathlib.Data.Ordmap.Ordnode Mathlib.Data.PEquiv Mathlib.Data.PNat.Defs Mathlib.Data.PNat.Equiv Mathlib.Data.PSigma.Order Mathlib.Data.Part Mathlib.Data.Rat.Defs Mathlib.Data.Set.Basic Mathlib.Data.Set.Disjoint Mathlib.Data.Set.Enumerate Mathlib.Data.Set.Inclusion Mathlib.Data.Set.Insert Mathlib.Data.Set.Order Mathlib.Data.Set.Subsingleton Mathlib.Data.SetLike.Basic Mathlib.Data.Sigma.Order Mathlib.Data.String.Basic Mathlib.Data.Sum.Lattice Mathlib.Data.Sum.Order Mathlib.InformationTheory.Coding.UniquelyDecodable Mathlib.Logic.Function.FiberPartition Mathlib.Order.Antisymmetrization Mathlib.Order.Basic Mathlib.Order.BooleanAlgebra.Basic Mathlib.Order.BooleanAlgebra.Defs Mathlib.Order.Booleanisation Mathlib.Order.BoundedOrder.Basic Mathlib.Order.BoundedOrder.Lattice Mathlib.Order.BoundedOrder.Monotone Mathlib.Order.Circular Mathlib.Order.Comparable Mathlib.Order.Compare Mathlib.Order.Disjoint Mathlib.Order.GaloisConnection.Defs Mathlib.Order.Heyting.Basic Mathlib.Order.Heyting.Boundary Mathlib.Order.Heyting.Hom Mathlib.Order.Hom.Basic Mathlib.Order.Hom.BoundedLattice Mathlib.Order.Hom.Bounded Mathlib.Order.Hom.Lattice Mathlib.Order.Hom.WithTopBot Mathlib.Order.Iterate Mathlib.Order.Lattice Mathlib.Order.Lex Mathlib.Order.Max Mathlib.Order.MinMax Mathlib.Order.Monotone.Basic Mathlib.Order.Monotone.Defs Mathlib.Order.Monotone.Monovary Mathlib.Order.Nat Mathlib.Order.OrderDual Mathlib.Order.Part Mathlib.Order.PropInstances Mathlib.Order.RelClasses Mathlib.Order.RelIso.Basic Mathlib.Order.SetIsMax Mathlib.Order.SymmDiff Mathlib.Order.Synonym Mathlib.Order.Types.Defs Mathlib.Order.ULift Mathlib.Order.WithBotTop Mathlib.Order.WithBot Mathlib.SetTheory.Lists Mathlib.Tactic.ApplyFun Mathlib.Tactic.CategoryTheory.Monoidal.Basic Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes Mathlib.Tactic.CategoryTheory.Monoidal.Normalize Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence Mathlib.Tactic.CategoryTheory.MonoidalComp Mathlib.Tactic.Widget.StringDiagram Mathlib.Tactic.Zify

1

---

Declarations diff

+ PartialOrder.ofSetLikeAux
+ instance (A : Type*) : PartialOrder (tree A) := fast_instance% .ofSetLike (tree A) (List A)
+ instance (G : Type*) [CommGroup G] : PartialOrder (GroupCone G) := fast_instance% .ofSetLike (GroupCone G) G
+ instance (R : Type*) [Ring R] : PartialOrder (RingCone R) := fast_instance% .ofSetLike (RingCone R) R
+ instance : PartialOrder (AffineSubspace k P) := fast_instance% .ofSetLike (AffineSubspace k P) P
+ instance : PartialOrder (BooleanSubalgebra α) := fast_instance% .ofSetLike (BooleanSubalgebra α) α
+ instance : PartialOrder (ClopenUpperSet α) := fast_instance% .ofSetLike (ClopenUpperSet α) α
+ instance : PartialOrder (Clopens α) := fast_instance% .ofSetLike (Clopens α) α
+ instance : PartialOrder (ClosedSubgroup G) := fast_instance% .ofSetLike (ClosedSubgroup G) G
+ instance : PartialOrder (ClosedSubmodule R M) := fast_instance% .ofSetLike (ClosedSubmodule R M) M
+ instance : PartialOrder (Closeds α) := fast_instance% .ofSetLike (Closeds α) α
+ instance : PartialOrder (CompactOpens α) := fast_instance% .ofSetLike (CompactOpens α) α
+ instance : PartialOrder (Compacts α) := fast_instance% .ofSetLike (Compacts α) α
+ instance : PartialOrder (CompleteSublattice α) := fast_instance% .ofSetLike (CompleteSublattice α) α
+ instance : PartialOrder (ConvexBody V) := fast_instance% .ofSetLike (ConvexBody V) V
+ instance : PartialOrder (ConvexCone R M) := fast_instance% .ofSetLike (ConvexCone R M) M
+ instance : PartialOrder (FiniteIndexNormalSubgroup G) := fast_instance% .ofSetLike (FiniteIndexNormalSubgroup G) G
+ instance : PartialOrder (Finset α) := fast_instance% .ofSetLike (Finset α) α
+ instance : PartialOrder (Flag α) := fast_instance% .ofSetLike (Flag α) α
+ instance : PartialOrder (FractionalIdeal S P) := fast_instance% .ofSetLike (FractionalIdeal S P) P
+ instance : PartialOrder (G.ComponentCompl K) := fast_instance% .ofSetLike (G.ComponentCompl K) V
+ instance : PartialOrder (HomogeneousIdeal 𝒜) := fast_instance% .ofSetLike (HomogeneousIdeal 𝒜) A
+ instance : PartialOrder (HomogeneousSubsemiring 𝒜) := fast_instance% .ofSetLike (HomogeneousSubsemiring 𝒜) A
+ instance : PartialOrder (Ideal P) := fast_instance% .ofSetLike (Ideal P) P
+ instance : PartialOrder (IntermediateField K L) := fast_instance% .ofSetLike (IntermediateField K L) L
+ instance : PartialOrder (IrreducibleCloseds α) := fast_instance% .ofSetLike (IrreducibleCloseds α) α
+ instance : PartialOrder (L.DefinableSet A α) := fast_instance% .ofSetLike (L.DefinableSet A α) (α → M)
+ instance : PartialOrder (L.ElementarySubstructure M) := fast_instance% .ofSetLike (L.ElementarySubstructure M) M
+ instance : PartialOrder (L.Substructure M) := fast_instance% .ofSetLike (L.Substructure M) M
+ instance : PartialOrder (LieSubalgebra R L) := fast_instance% .ofSetLike (LieSubalgebra R L) L
+ instance : PartialOrder (LieSubmodule R L M) := fast_instance% .ofSetLike (LieSubmodule R L M) M
+ instance : PartialOrder (MySubobject X) := fast_instance% .ofSetLike (MySubobject X) X
+ instance : PartialOrder (NonUnitalStarSubalgebra R A) := fast_instance% .ofSetLike (NonUnitalStarSubalgebra R A) A
+ instance : PartialOrder (NonUnitalSubalgebra R A) := fast_instance% .ofSetLike (NonUnitalSubalgebra R A) A
+ instance : PartialOrder (NonUnitalSubring R) := fast_instance% .ofSetLike (NonUnitalSubring R) R
+ instance : PartialOrder (NonUnitalSubsemiring R) := fast_instance% .ofSetLike (NonUnitalSubsemiring R) R
+ instance : PartialOrder (NonemptyCompacts α) := fast_instance% .ofSetLike (NonemptyCompacts α) α
+ instance : PartialOrder (OpenNhdsOf x) := fast_instance% .ofSetLike (OpenNhdsOf x) α
+ instance : PartialOrder (OpenNormalSubgroup G) := fast_instance% .ofSetLike (OpenNormalSubgroup G) G
+ instance : PartialOrder (OpenSubgroup G) := fast_instance% .ofSetLike (OpenSubgroup G) G
+ instance : PartialOrder (Opens α) := fast_instance% .ofSetLike (Opens α) α
+ instance : PartialOrder (PFilter P) := fast_instance% .ofSetLike (PFilter P) P
+ instance : PartialOrder (PositiveCompacts α) := fast_instance% .ofSetLike (PositiveCompacts α) α
+ instance : PartialOrder (ProperCone R E) := fast_instance% .ofSetLike (ProperCone R E) E
+ instance : PartialOrder (RelUpperSet P) := fast_instance% .ofSetLike (RelUpperSet P) α
+ instance : PartialOrder (RingPreordering R) := fast_instance% .ofSetLike (RingPreordering R) R
+ instance : PartialOrder (SaturatedSubmonoid M) := fast_instance% .ofSetLike ..
+ instance : PartialOrder (Set.powersetCard α n) := fast_instance% .ofSetLike (Set.powersetCard α n) α
+ instance : PartialOrder (StarSubalgebra R A) := fast_instance% .ofSetLike (StarSubalgebra R A) A
+ instance : PartialOrder (SubDPIdeal hI) := fast_instance% .ofSetLike (SubDPIdeal hI) A
+ instance : PartialOrder (SubMulAction R M) := fast_instance% .ofSetLike (SubMulAction R M) M
+ instance : PartialOrder (SubObj X) := fast_instance% .ofSetLike (SubObj X) X
+ instance : PartialOrder (Subalgebra R A) := fast_instance% .ofSetLike (Subalgebra R A) A
+ instance : PartialOrder (Subcomplex C) := fast_instance% .ofSetLike (Subcomplex C) X
+ instance : PartialOrder (Subfield K) := fast_instance% .ofSetLike (Subfield K) K
+ instance : PartialOrder (Subgroup G) := fast_instance% .ofSetLike (Subgroup G) G
+ instance : PartialOrder (Subgroupoid C) := fast_instance% .ofSetLike (Subgroupoid C) (Σ c d : C, c ⟶ d)
+ instance : PartialOrder (Sublattice α) := fast_instance% .ofSetLike (Sublattice α) α
+ instance : PartialOrder (Sublocale X) := fast_instance% .ofSetLike (Sublocale X) X
+ instance : PartialOrder (Submodule R M) := fast_instance% .ofSetLike (Submodule R M) M
+ instance : PartialOrder (Submonoid M) := fast_instance% .ofSetLike (Submonoid M) M
+ instance : PartialOrder (Subrepresentation ρ) := fast_instance% .ofSetLike (Subrepresentation ρ) W
+ instance : PartialOrder (Subring R) := fast_instance% .ofSetLike (Subring R) R
+ instance : PartialOrder (Subsemigroup M) := fast_instance% .ofSetLike (Subsemigroup M) M
+ instance : PartialOrder (Subsemiring R) := fast_instance% .ofSetLike (Subsemiring R) R
+ instance : PartialOrder (Subspace K V) := fast_instance% .ofSetLike (Subspace K V) (ℙ K V)
+ instance : PartialOrder (Sylow p G) := fast_instance% .ofSetLike (Sylow p G) G
+ instance : PartialOrder (Sym2 α) := fast_instance% .ofSetLike (Sym2 α) α
+ instance : PartialOrder (T.CompleteType α) := fast_instance% .ofSetLike (T.CompleteType α) (L[[α]].Sentence)
+ instance : PartialOrder (TwoSidedIdeal R) := fast_instance% .ofSetLike (TwoSidedIdeal R) R
+ instance : PartialOrder (ValuationSubring K) := fast_instance% .ofSetLike (ValuationSubring K) K
+ instance : PartialOrder (VonNeumannAlgebra H) := fast_instance% .ofSetLike (VonNeumannAlgebra H) (H →L[ℂ] H)
+ instance : PartialOrder YoungDiagram := fast_instance% .ofSetLike YoungDiagram (ℕ × ℕ)
+ instance : PartialOrder ZFSet.{u} := fast_instance% .ofSetLike ZFSet.{u} ZFSet.{u}
+ instance [DecidableEq X] : PartialOrder (DecSubObj X) := fast_instance% .ofSetLike (DecSubObj X) X
+ instance {α : Type*} [LE α] : PartialOrder (NonemptyChain α) := fast_instance% .ofSetLike (NonemptyChain α) α
++ instance : PartialOrder (HomogeneousSubmodule 𝒜 ℳ) := fast_instance% .ofSetLike (HomogeneousSubmodule 𝒜 ℳ) M
- instance (A : Type*) : PartialOrder (tree A) := .ofSetLike (tree A) (List A)
- instance (G : Type*) [CommGroup G] : PartialOrder (GroupCone G) := .ofSetLike (GroupCone G) G
- instance (R : Type*) [Ring R] : PartialOrder (RingCone R) := .ofSetLike (RingCone R) R
- instance : PartialOrder (AffineSubspace k P) := .ofSetLike (AffineSubspace k P) P
- instance : PartialOrder (BooleanSubalgebra α) := .ofSetLike (BooleanSubalgebra α) α
- instance : PartialOrder (ClopenUpperSet α) := .ofSetLike (ClopenUpperSet α) α
- instance : PartialOrder (Clopens α) := .ofSetLike (Clopens α) α
- instance : PartialOrder (ClosedSubgroup G) := .ofSetLike (ClosedSubgroup G) G
- instance : PartialOrder (ClosedSubmodule R M) := .ofSetLike (ClosedSubmodule R M) M
- instance : PartialOrder (Closeds α) := .ofSetLike (Closeds α) α
- instance : PartialOrder (CompactOpens α) := .ofSetLike (CompactOpens α) α
- instance : PartialOrder (Compacts α) := .ofSetLike (Compacts α) α
- instance : PartialOrder (CompleteSublattice α) := .ofSetLike (CompleteSublattice α) α
- instance : PartialOrder (ConvexBody V) := .ofSetLike (ConvexBody V) V
- instance : PartialOrder (ConvexCone R M) := .ofSetLike (ConvexCone R M) M
- instance : PartialOrder (FiniteIndexNormalSubgroup G) := .ofSetLike (FiniteIndexNormalSubgroup G) G
- instance : PartialOrder (Finset α) := .ofSetLike (Finset α) α
- instance : PartialOrder (Flag α) := .ofSetLike (Flag α) α
- instance : PartialOrder (FractionalIdeal S P) := .ofSetLike (FractionalIdeal S P) P
- instance : PartialOrder (G.ComponentCompl K) := .ofSetLike (G.ComponentCompl K) V
- instance : PartialOrder (HomogeneousIdeal 𝒜) := .ofSetLike (HomogeneousIdeal 𝒜) A
- instance : PartialOrder (HomogeneousSubsemiring 𝒜) := .ofSetLike (HomogeneousSubsemiring 𝒜) A
- instance : PartialOrder (Ideal P) := .ofSetLike (Ideal P) P
- instance : PartialOrder (IntermediateField K L) := .ofSetLike (IntermediateField K L) L
- instance : PartialOrder (IrreducibleCloseds α) := .ofSetLike (IrreducibleCloseds α) α
- instance : PartialOrder (L.DefinableSet A α) := .ofSetLike (L.DefinableSet A α) (α → M)
- instance : PartialOrder (L.ElementarySubstructure M) := .ofSetLike (L.ElementarySubstructure M) M
- instance : PartialOrder (L.Substructure M) := .ofSetLike (L.Substructure M) M
- instance : PartialOrder (LieSubalgebra R L) := .ofSetLike (LieSubalgebra R L) L
- instance : PartialOrder (LieSubmodule R L M) := .ofSetLike (LieSubmodule R L M) M
- instance : PartialOrder (MySubobject X) := .ofSetLike (MySubobject X) X
- instance : PartialOrder (NonUnitalStarSubalgebra R A) := .ofSetLike (NonUnitalStarSubalgebra R A) A
- instance : PartialOrder (NonUnitalSubalgebra R A) := .ofSetLike (NonUnitalSubalgebra R A) A
- instance : PartialOrder (NonUnitalSubring R) := .ofSetLike (NonUnitalSubring R) R
- instance : PartialOrder (NonUnitalSubsemiring R) := .ofSetLike (NonUnitalSubsemiring R) R
- instance : PartialOrder (NonemptyCompacts α) := .ofSetLike (NonemptyCompacts α) α
- instance : PartialOrder (OpenNhdsOf x) := .ofSetLike (OpenNhdsOf x) α
- instance : PartialOrder (OpenNormalSubgroup G) := .ofSetLike (OpenNormalSubgroup G) G
- instance : PartialOrder (OpenSubgroup G) := .ofSetLike (OpenSubgroup G) G
- instance : PartialOrder (Opens α) := .ofSetLike (Opens α) α
- instance : PartialOrder (PFilter P) := .ofSetLike (PFilter P) P
- instance : PartialOrder (PositiveCompacts α) := .ofSetLike (PositiveCompacts α) α
- instance : PartialOrder (ProperCone R E) := .ofSetLike (ProperCone R E) E
- instance : PartialOrder (RelUpperSet P) := .ofSetLike (RelUpperSet P) α
- instance : PartialOrder (RingPreordering R) := .ofSetLike (RingPreordering R) R
- instance : PartialOrder (SaturatedSubmonoid M) := .ofSetLike ..
- instance : PartialOrder (Set.powersetCard α n) := .ofSetLike (Set.powersetCard α n) α
- instance : PartialOrder (StarSubalgebra R A) := .ofSetLike (StarSubalgebra R A) A
- instance : PartialOrder (SubDPIdeal hI) := .ofSetLike (SubDPIdeal hI) A
- instance : PartialOrder (SubMulAction R M) := .ofSetLike (SubMulAction R M) M
- instance : PartialOrder (SubObj X) := .ofSetLike (SubObj X) X
- instance : PartialOrder (Subalgebra R A) := .ofSetLike (Subalgebra R A) A
- instance : PartialOrder (Subcomplex C) := .ofSetLike (Subcomplex C) X
- instance : PartialOrder (Subfield K) := .ofSetLike (Subfield K) K
- instance : PartialOrder (Subgroup G) := .ofSetLike (Subgroup G) G
- instance : PartialOrder (Subgroupoid C) := .ofSetLike (Subgroupoid C) (Σ c d : C, c ⟶ d)
- instance : PartialOrder (Sublattice α) := .ofSetLike (Sublattice α) α
- instance : PartialOrder (Sublocale X) := .ofSetLike (Sublocale X) X
- instance : PartialOrder (Submodule R M) := .ofSetLike (Submodule R M) M
- instance : PartialOrder (Submonoid M) := .ofSetLike (Submonoid M) M
- instance : PartialOrder (Subrepresentation ρ) := .ofSetLike (Subrepresentation ρ) W
- instance : PartialOrder (Subring R) := .ofSetLike (Subring R) R
- instance : PartialOrder (Subsemigroup M) := .ofSetLike (Subsemigroup M) M
- instance : PartialOrder (Subsemiring R) := .ofSetLike (Subsemiring R) R
- instance : PartialOrder (Subspace K V) := .ofSetLike (Subspace K V) (ℙ K V)
- instance : PartialOrder (Sylow p G) := .ofSetLike (Sylow p G) G
- instance : PartialOrder (Sym2 α) := .ofSetLike (Sym2 α) α
- instance : PartialOrder (T.CompleteType α) := .ofSetLike (T.CompleteType α) (L[[α]].Sentence)
- instance : PartialOrder (TwoSidedIdeal R) := .ofSetLike (TwoSidedIdeal R) R
- instance : PartialOrder (ValuationSubring K) := .ofSetLike (ValuationSubring K) K
- instance : PartialOrder (VonNeumannAlgebra H) := .ofSetLike (VonNeumannAlgebra H) (H →L[ℂ] H)
- instance : PartialOrder YoungDiagram := .ofSetLike YoungDiagram (ℕ × ℕ)
- instance : PartialOrder ZFSet.{u} := .ofSetLike ZFSet.{u} ZFSet.{u}
- instance [DecidableEq X] : PartialOrder (DecSubObj X) := .ofSetLike (DecSubObj X) X
- instance {α : Type*} [LE α] : PartialOrder (NonemptyChain α) := .ofSetLike (NonemptyChain α) α
-- instance : PartialOrder (HomogeneousSubmodule 𝒜 ℳ) := .ofSetLike (HomogeneousSubmodule 𝒜 ℳ) M

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[sgouezel]

!radar

[leanprover-radar]

Benchmark results for 3b2db21 against df818bb are in. Significant changes detected! @sgouezel

• 🟥 main exited with code 1

No significant changes detected.

[sgouezel]

!radar

[leanprover-radar]

Benchmark results for bd4e9e9 against df818bb are in. There are no significant changes. @sgouezel

• 🟥 build//instructions: +7.4G (+0.00%)

No significant changes detected.

[eric-wieser]

My memory is that fast_instance is only helpful if you're constructing a StrongFoo X instance and you previously created a WeakFoo X higher up the file; that is, it's useless when transferring the root typeclass in a hierarchy, and provides value for all the ones that follow