mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.mk.inj : ∀ {α β σ : Type} {descr : Lean.ScopedEnvExtension.Descr α β σ}
  {ext :
    Lean.PersistentEnvExtension (Lean.ScopedEnvExtension.Entry α) (Lean.ScopedEnvExtension.Entry β)
      (Lean.ScopedEnvExtension.StateStack α β σ)}
  {descr_1 : Lean.ScopedEnvExtension.Descr α β σ}
  {ext_1 :
    Lean.PersistentEnvExtension (Lean.ScopedEnvExtension.Entry α) (Lean.ScopedEnvExtension.Entry β)
      (Lean.ScopedEnvExtension.StateStack α β σ)},
  { descr := descr, ext := ext } = { descr := descr_1, ext := ext_1 } → descr = descr_1 ∧ ext = ext_1
-- Lean.Elab.ParseImportsFast
Lean.PrintImportsResult.mk.sizeOf_spec : ∀ (imports : Array Lean.PrintImportResult), sizeOf { imports := imports } = 1 + sizeOf imports
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The projection map from the relative cotangent space to the module of differentials.  -/
Algebra.Extension.toKaehler : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (P : Algebra.Extension R S) → P.CotangentSpace →ₗ[S] Ω[S⁄R]
-- Init.Prelude
/-- A possible binding of an identifier in the context in which it was quoted.

Identifiers in quotations may refer to either global declarations or to namespaces that are in scope
at the site of the quotation. These are saved in the `Syntax.ident` constructor and are part of the
implementation of hygienic macros.
 -/
Lean.Syntax.Preresolved : Type
-- Init.System.IO
/-- Removes (deletes) a directory.

Removing a directory fails if the directory is not empty. Use `IO.FS.removeDirAll` to remove
directories along with their contents.
 -/
IO.FS.removeDir : System.FilePath → IO Unit
-- Mathlib.Algebra.Group.Units.Hom
Units.coeHom_injective : ∀ {M : Type u} [inst : Monoid M], Function.Injective ⇑(Units.coeHom M)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, (t.insert k).max! = t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Order.SuccPred.InitialSeg
/-- **Alias** of the reverse direction of `PrincipalSeg.isSuccLimit_apply_iff`. -/
PrincipalSeg.map_isSuccLimit : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α <i β),
  Order.IsSuccLimit a → Order.IsSuccLimit (f.toRelEmbedding a)
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- An open set in `OnePoint X` constructed from a closed compact set in `X`  -/
OnePoint.opensOfCompl : {X : Type u_1} →
  [inst : TopologicalSpace X] → (s : Set X) → IsClosed s → IsCompact s → TopologicalSpace.Opens (OnePoint X)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.instInhabitedRing : Inhabited Lean.Meta.Sym.Arith.Ring
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₂₃).toFunctor.obj ((F.map f₀₂).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X) h) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp
        ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)) h)
-- Mathlib.Topology.Category.TopPair
/-- If we have a `Homotopy g₀ g₁` and a `Homotopy f₀ f₁`, we can define a
`Homotopy (f₀ ≫ g₀) (f₁ ≫ g₁)` by `TopCat.Homotopy.comp` on the first and second components.
 -/
TopPair.Homotopy.comp : {X Y Z : TopPair} →
  {f₀ f₁ : X ⟶ Y} →
    {g₀ g₁ : Y ⟶ Z} →
      TopPair.Homotopy g₀ g₁ →
        TopPair.Homotopy f₀ f₁ →
          TopPair.Homotopy (CategoryTheory.CategoryStruct.comp f₀ g₀) (CategoryTheory.CategoryStruct.comp f₁ g₁)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- Given two classes of morphisms `W₁` and `W₂` on a category `C`, this is
the data of the factorization of a morphism `f : X ⟶ Y` as `i ≫ p` with
`W₁ i` and `W₂ p`.  -/
CategoryTheory.MorphismProperty.MapFactorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → {X Y : C} → (X ⟶ Y) → Type (max u_1 v_1)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- External multiplication of a `f : M →ₚₗ[R] N` by `r : R`  -/
PolynomialLaw.smul : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → R → (M →ₚₗ[R] N) → M →ₚₗ[R] N
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
/-- A finite measure `μ` over `X × Y` is determined by the values `∫ p, f p.1 * g p.2 ∂μ`,
for `f : X → ℝ` and `g : Y → ℝ` any bounded continuous functions.  -/
Measure.ext_of_integral_mul_boundedContinuousFunction : ∀ {Z : Type u_3} {T : Type u_4} {mZ : MeasurableSpace Z} [inst : TopologicalSpace Z] [BorelSpace Z]
  [HasOuterApproxClosed Z] {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T]
  [HasOuterApproxClosed T] {μ ν : MeasureTheory.Measure (Z × T)} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  (∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : Z × T), f p.1 * g p.2 ∂μ = ∫ (p : Z × T), f p.1 * g p.2 ∂ν) →
    μ = ν
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.clift_apply_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : FreeMonoid (M ⊕ N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1)
  (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y)))
  (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y)))
  (x : M), (Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inl x) = f (FreeMonoid.of (Sum.inl x))
-- Init.Data.Nat.Lemmas
Nat.lt_of_pow_dvd_right : ∀ {b a n : ℕ}, b ≠ 0 → 2 ≤ a → a ^ n ∣ b → n < b
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- An `AddSubmonoid` of an ordered cancellative additive monoid is an ordered cancellative
additive monoid.  -/
AddSubmonoidClass.toIsOrderedCancelAddMonoid : ∀ {M : Type u_1} {S : Type u_2} [inst : SetLike S M] [inst_1 : AddCommMonoid M] [inst_2 : Preorder M]
  [IsOrderedCancelAddMonoid M] [inst_4 : AddSubmonoidClass S M] (s : S), IsOrderedCancelAddMonoid ↥s
-- Mathlib.Algebra.Ring.Invertible
IsAddUnit.mul_left : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] {x : R}, IsAddUnit x → ∀ (y : R), IsAddUnit (y * x)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_id_range_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_6}
  {f : ι → M}, Function.Injective f → (LinearIndepOn R id (Set.range f) ↔ LinearIndependent R f)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralNorm_one : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L], spectralNorm K L 1 = 1
-- Mathlib.Order.Category.BoolAlg
BoolAlg.ofHom_id : ∀ {X : Type u} [inst : BooleanAlgebra X],
  BoolAlg.ofHom (BoundedLatticeHom.id X) = CategoryTheory.CategoryStruct.id { carrier := X, str := inst }
-- Lean.Elab.Binders
/-- Same as `elabBinder` with a single binder. -/
Lean.Elab.Term.elabBinder : {α : Type} → Lean.Syntax → (Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Topology.Algebra.InfiniteSum.Group
multipliable_congr_atTop : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f₁ g₁ : ℕ → α},
  f₁ =ᶠ[Filter.atTop] g₁ → (Multipliable f₁ ↔ Multipliable g₁)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- The forgetful functor from commutative group objects to commutative monoid objects is fully
faithful.  -/
CategoryTheory.CommGrp.fullyFaithfulForget₂CommMon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (CategoryTheory.CommGrp.forget₂CommMon C).FullyFaithful
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
IntermediateField.adjoin_rootSet_isSplittingField : ∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {p : Polynomial K},
  (Polynomial.map (algebraMap K L) p).Splits →
    Polynomial.IsSplittingField K (↥(IntermediateField.adjoin K (p.rootSet L))) p
-- Mathlib.Topology.MetricSpace.Bounded
Metric.cobounded_le_cocompact : ∀ {α : Type u} [inst : PseudoMetricSpace α], Bornology.cobounded α ≤ Filter.cocompact α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, (Std.TreeMap.map f t).contains k = t.contains k
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_injective : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) {R : ℝ}, R ≠ 0 → Function.Injective (EuclideanGeometry.inversion c R)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} →
              (t : Lean.Meta.Grind.Arith.Linear.UnsatProof) →
                ((t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t) →
                  ((t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t) →
                    ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t) →
                      ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t) →
                        ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t) →
                          ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t) →
                            ((t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t) →
                              motive_7 t ×' t.below
-- Mathlib.Order.Filter.Pointwise
Filter.map_add : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : Add β] {f₁ f₂ : Filter α}
  [inst_2 : FunLike F α β] [AddHomClass F α β] (m : F),
  Filter.map (⇑m) (f₁ + f₂) = Filter.map (⇑m) f₁ + Filter.map (⇑m) f₂
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- Distance on `GHSpace`: the distance between two nonempty compact spaces is the infimum
Hausdorff distance between isometric copies of the two spaces in a metric space. For the definition,
we only consider embeddings in `ℓ^∞(ℝ)`, but we will prove below that it works for all spaces.  -/
GromovHausdorff.instDistGHSpace : Dist GromovHausdorff.GHSpace
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.below.top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → J.Saturate X a → Prop} (X : C),
  CategoryTheory.Precoverage.Saturate.below ⋯
-- Mathlib.Data.Stream.Init
Stream'.iterate.eq_2 : ∀ {α : Type u} (f : α → α) (a : α) (n : ℕ), Stream'.iterate f a n.succ = f (Stream'.iterate f a n)
-- Aesop.Script.ScriptM
Aesop.recordScriptStep : {m : Type → Type u_1} → [MonadStateOf (Array Aesop.Script.LazyStep) m] → Aesop.Script.LazyStep → m Unit
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtensionId : ∀ {C : Type u_1} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] (F₀ : CategoryTheory.Functor C H),
  F₀.IsLeftKanExtension F₀.leftUnitor.inv
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_vadd' : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [inst : VAdd M β] (c : α → M) (f : α → β),
  ↑(c +ᵥ f) = ↑c +ᵥ ↑f
-- Aesop.Forward.SlotIndex
Aesop.instDecidableRelSlotIndexLt : DecidableRel fun x1 x2 => x1 < x2
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.con.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal],
  QuotientAddGroup.con N = { toSetoid := QuotientAddGroup.leftRel N, add' := ⋯ }
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.surjective : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  Function.Surjective ⇑e
-- Lean.Meta.Tactic.Grind.EMatch
/-- Internal "marker" for representing equality proofs for generalized patterns.
They must be synthesized after we have the partial assignment.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.delayedEqProof : Lean.Expr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeId.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.Cone.postcomposeId =
    CategoryTheory.NatIso.ofComponents
      (fun s =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl
            ((CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.id F)).obj s).pt)
          ⋯)
      ⋯
-- Lean.Expr
Lean.Int.mkInstMod : Lean.Expr
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F)
  (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift F c)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) =
    CategoryTheory.CategoryStruct.comp (c.π.app j) h
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁`
contained in it, the dimensions of `K₁` and the intersection of its
orthogonal subspace with `K₂` add to that of `K₂`.  -/
Submodule.finrank_add_inf_finrank_orthogonal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₁ K₂ : Submodule 𝕜 E} [FiniteDimensional 𝕜 ↥K₂],
  K₁ ≤ K₂ → ∀ {n : ℕ}, Module.finrank 𝕜 ↥K₁ + n = Module.finrank 𝕜 ↥K₂ → Module.finrank 𝕜 ↥(K₁ᗮ ⊓ K₂) = n
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.instEquivLike.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N],
  ContinuousAddEquiv.instEquivLike =
    { coe := fun f => f.toFun, inv := fun f => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).get? k' =
        if h : compare k k' = Ordering.eq then cast ⋯ (f (t.get? k)) else t.get? k'
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.rightKanExtensionUnique.congr_simp : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α α_1 : L.comp F' ⟶ F) (e_α : α = α_1) [inst_3 : F'.IsRightKanExtension α] (F'' : CategoryTheory.Functor D H)
  (α' α'_1 : L.comp F'' ⟶ F) (e_α' : α' = α'_1) [inst_4 : F''.IsRightKanExtension α'],
  F'.rightKanExtensionUnique α F'' α' = F'.rightKanExtensionUnique α_1 F'' α'_1
-- Mathlib.Order.Atoms
/-- An order is strongly coatomic if every nontrivial interval `[a, b]`
contains an element covered by `b`.  -/
IsStronglyCoatomic : (α : Type u_5) → [Preorder α] → Prop
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.ext : ∀ {C : Type u} {x y : CategoryTheory.LocallyDiscrete C}, x.as = y.as → x = y
-- Mathlib.Order.Filter.Basic
Filter.instTransForallEventuallyLEEventuallyEq : {α : Type u} →
  {β : Type v} →
    [inst : Preorder β] →
      {l : Filter α} → Trans (fun x1 x2 => x1 ≤ᶠ[l] x2) (fun x1 x2 => x1 =ᶠ[l] x2) fun x1 x2 => x1 ≤ᶠ[l] x2
-- Init.Data.UInt.Lemmas
UInt8.toNat_mod_uSizeSize : ∀ (n : UInt8), n.toNat % USize.size = n.toNat
-- Mathlib.Order.Shrink
/-- The order isomorphism `α ≃o Shrink.{u} α`.  -/
orderIsoShrink : (α : Type u_1) → [inst : Small.{u, u_1} α] → [inst_1 : Preorder α] → α ≃o Shrink.{u, u_1} α
-- Std.Sat.AIG.RelabelNat
_private.Std.Sat.AIG.RelabelNat.0.Std.Sat.AIG.RelabelNat.State.ofAIGAux.go.match_1.eq_1 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (a : α)
  (h_1 : (a_1 : α) → Std.Sat.AIG.Decl.atom a = Std.Sat.AIG.Decl.atom a_1 → motive (Std.Sat.AIG.Decl.atom a_1))
  (h_2 : Std.Sat.AIG.Decl.atom a = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.atom a = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match hdecl : Std.Sat.AIG.Decl.atom a with
    | Std.Sat.AIG.Decl.atom a_1 => h_1 a_1 hdecl
    | Std.Sat.AIG.Decl.false => h_2 hdecl
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs hdecl) =
    h_1 a ⋯
-- Init.Data.SInt.Lemmas
Int32.toISize_ofBitVec : ∀ (b : BitVec 32), (Int32.ofBitVec b).toISize = ISize.ofBitVec (BitVec.signExtend System.Platform.numBits b)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeLimitClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (J : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J], (P.limitClosure J).IsClosedUnderLimitsOfShape J
-- Mathlib.RingTheory.Regular.ProjectiveDimension
ModuleCat.hasProjectiveDimensionLT_of_forall_finite : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M]
  (n : ℕ),
  (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (CategoryTheory.Abelian.Ext M L n)) →
    CategoryTheory.HasProjectiveDimensionLT M n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {h' : k ∈ Std.DHashMap.filterMap f m},
  (Std.DHashMap.filterMap f m).get k h' = (f k (m.get k ⋯)).get ⋯
-- Mathlib.Logic.Equiv.Defs
/-- `α` is equivalent to an empty type iff `α` is empty.  -/
Equiv.equivEmptyEquiv : (α : Sort u) → α ≃ Empty ≃ IsEmpty α
-- Init.Data.BitVec.Basic
/-- Concatenates `i` copies of `x` into a new vector of length `w * i`.  -/
BitVec.replicate : {w : ℕ} → (i : ℕ) → BitVec w → BitVec (w * i)
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Bound.le.sizeOf_spec : ∀ (n : ℤ), sizeOf (Mathlib.Tactic.IntervalCases.Bound.le n) = 1 + sizeOf n
-- Mathlib.Data.Set.Image
/-- A variant of `range_coe`. Try to use `range_coe` if possible.
This version is useful when defining a new type that is defined as the subtype of something.
In that case, the coercion doesn't fire anymore.  -/
Subtype.range_val : ∀ {α : Type u_1} {s : Set α}, Set.range Subtype.val = s
-- Mathlib.LinearAlgebra.Ray
RayVector.coe_equiv_symm : ∀ {R : Type u_1} {M : Type u_2} [inst : Zero M] {v : M} (h : v ≠ 0),
  ↑((RayVector.equiv R M) ((RayVector.equiv R M).symm ⟨v, h⟩)) = v
-- Mathlib.Algebra.GroupWithZero.Units.Basic
inv_pow_sub₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} {m n : ℕ}, a ≠ 0 → n ≤ m → a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
-- Mathlib.Geometry.Polygon.Basic
Polygon.mk.inj : ∀ {P : Type u_1} {n : ℕ} {vertices vertices_1 : Fin n → P},
  { vertices := vertices } = { vertices := vertices_1 } → vertices = vertices_1
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.isoApp_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁ ≅ C₂) (i : ι), (HomologicalComplex.Hom.isoApp f i).hom = f.hom.f i
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Poly.denote.match_1.eq_2 : ∀ (motive : Nat.Internal.Linear.Poly → Sort u_1) (k : ℕ) (v : Nat.Internal.Linear.Var)
  (p : List (ℕ × Nat.Internal.Linear.Var)) (h_1 : Unit → motive [])
  (h_2 : (k : ℕ) → (v : Nat.Internal.Linear.Var) → (p : List (ℕ × Nat.Internal.Linear.Var)) → motive ((k, v) :: p)),
  (match (k, v) :: p with
    | [] => h_1 ()
    | (k, v) :: p => h_2 k v p) =
    h_2 k v p
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If `F` preserves the limit of the pair `(A, B)`, then `prodComparison F A B` is an isomorphism.
 -/
CategoryTheory.CartesianMonoidalCategory.prodComparisonIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              (A B : C) →
                [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F] →
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj A B) ≅
                    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Given a function `m : ℝ≥0∞ → ℝ≥0∞` and `r > 0`, let `μ r` be the maximal outer measure such that
`μ s ≤ m (ediam s)` whenever `ediam s < r`. Then `mkMetric m = ⨆ r > 0, μ r`.  -/
MeasureTheory.OuterMeasure.mkMetric : {X : Type u_2} → [EMetricSpace X] → (ENNReal → ENNReal) → MeasureTheory.OuterMeasure X
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- compatibility of the given morphism with the given idempotents  -/
CategoryTheory.Idempotents.Karoubi.Hom.comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (self : P.Hom Q), CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp self.f Q.p) = self.f
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- See Note [custom simps projection].  -/
DilationEquiv.Simps.symm_apply : {X : Type u_1} → {Y : Type u_2} → [inst : PseudoEMetricSpace X] → [inst_1 : PseudoEMetricSpace Y] → X ≃ᵈ Y → Y → X