mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Do.WP.Basic
/-- Soundness of `pure`: the postcondition applied to `x` implies the weakest precondition of
`pure x`.  -/
Std.Internal.Do.WPMonad.pure_le_wp_pure : ∀ {m : Type u → Type v} {Pred : outParam (Type w)} {EPred : outParam (Type w')} {inst : Monad m}
  {inst_1 : Std.Internal.Do.Assertion Pred} {inst_2 : Std.Internal.Do.Assertion EPred}
  [self : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u} (x : α) (post : α → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel (post x) (Std.Internal.Do.wp (pure x) post epost)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.flipCompEvaluation_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (a : A) (X : B),
  (CategoryTheory.flipCompEvaluation F a).hom.app X = CategoryTheory.CategoryStruct.id ((F.obj a).obj X)
-- Mathlib.Computability.Partrec
Computable.encode_iff : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
  (Computable fun a => Encodable.encode (f a)) ↔ Computable f
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The function `sinKernel a` has exponential decay at `+∞`, for any `a`.  -/
HurwitzZeta.isBigO_atTop_sinKernel : ∀ (a : UnitAddCircle), ∃ p, 0 < p ∧ HurwitzZeta.sinKernel a =O[Filter.atTop] fun x => Real.exp (-p * x)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.image_map_comp_imageSubobjectIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X}
  [inst_1 : CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g]
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.map sq)
      (CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk g).hom).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv
      (CategoryTheory.Limits.imageSubobjectMap sq)
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceSemanticTokensParams : Lean.Lsp.FileSource Lean.Lsp.SemanticTokensParams
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getKey.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive : (t : Std.DTreeMap.Internal.Impl α β) → Std.DTreeMap.Internal.Impl.contains k t = true → Sort u_3) →
          (t : Std.DTreeMap.Internal.Impl α β) →
            (hlk : Std.DTreeMap.Internal.Impl.contains k t = true) →
              ((size : ℕ) →
                  (k' : α) →
                    (v : β k') →
                      (l r : Std.DTreeMap.Internal.Impl α β) →
                        (hlk :
                            Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
                              true) →
                          motive (Std.DTreeMap.Internal.Impl.inner size k' v l r) hlk) →
                motive t hlk
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.mk : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              (functor : A → CategoryTheory.Functor C D) →
                (shiftIso :
                    (n a a' : A) → n + a = a' → ((functor a').comp (CategoryTheory.shiftFunctor D n) ≅ functor a)) →
                  (∀ (a : A), shiftIso 0 a a ⋯ = (functor a).isoWhiskerLeft (CategoryTheory.shiftFunctorZero D A)) →
                    (∀ (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a''),
                        shiftIso (m + n) a a'' ⋯ =
                          (functor a'').isoWhiskerLeft (CategoryTheory.shiftFunctorAdd D m n) ≪≫
                            ((functor a'').associator (CategoryTheory.shiftFunctor D m)
                                  (CategoryTheory.shiftFunctor D n)).symm ≪≫
                              CategoryTheory.Functor.isoWhiskerRight (shiftIso m a' a'' ha'')
                                  (CategoryTheory.shiftFunctor D n) ≪≫
                                shiftIso n a a' ha') →
                      CategoryTheory.SingleFunctors C D A
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.ConnectedComponent.odd_oddComponents_ncard_subset_supp : ∀ {V : Type u} (G : SimpleGraph V) [Finite V] {G' : SimpleGraph V},
  G ≤ G' → ∀ (c' : G'.ConnectedComponent), Odd {c | c ∈ G.oddComponents ∧ c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Differentiable.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ g → (∀ (x : E), f x ≠ 0) → Differentiable ℝ fun x => f x ^ g x
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcKeepAliveParams.mk : Lean.Lsp.DocumentUri → UInt64 → Lean.Lsp.RpcKeepAliveParams
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {k a : α} {v : β}, (m.insert k v)[a]! = if (k == a) = true then v else m[a]!
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf_hom_app_app_hom_apply_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] (X : CategoryTheory.Sheaf J A) (X_1 : (CategoryTheory.Sheaf J A)ᵒᵖ)
  (a :
    (((CategoryTheory.sheafToPresheaf J A).comp
              (CategoryTheory.yoneda.comp
                ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J A)ᵒᵖ (CategoryTheory.Functor Cᵒᵖ A)ᵒᵖ
                      (Type (max u₁ v₂))).obj
                  (CategoryTheory.sheafToPresheaf J A).op))).obj
          X).obj
      X_1),
  ((CategoryTheory.ConcreteCategory.hom
          ((CategoryTheory.sheafToPresheafCompYonedaCompWhiskeringLeftSheafToPresheaf.hom.app X).app X_1))
        a).hom =
    (Equiv.ulift.toIso.inv.hom' a).down
-- Batteries.Data.BinomialHeap.Basic
/-- A `HeapNode` is one of the internal nodes of the binomial heap.
It is always a perfect binary tree, with the depth of the tree stored in the `Heap`.
However the interpretation of the two pointers is different: we view the `child`
as going to the first child of this node, and `sibling` goes to the next sibling
of this tree. So it actually encodes a forest where each node has children
`node.child`, `node.child.sibling`, `node.child.sibling.sibling`, etc.

Each edge in this forest denotes a `le a b` relation that has been checked, so
the root is smaller than everything else under it.
 -/
Batteries.BinomialHeap.Imp.HeapNode : Type u → Type u
-- Mathlib.Logic.Nontrivial.Defs
Decidable.exists_ne : ∀ {α : Type u_1} [Nontrivial α] [DecidableEq α] (x : α), ∃ y, y ≠ x
-- Mathlib.Algebra.FreeMonoid.Basic
/-- reverses the symbols in a free monoid element  -/
FreeMonoid.reverse : {α : Type u_1} → FreeMonoid α → FreeMonoid α
-- Mathlib.RingTheory.WittVector.Basic
WittVector.matrix_vecEmpty_coeff : ∀ {p : ℕ} {R : Type u_5} (i : Fin 0) (j : ℕ), (![] i).coeff j = ![] i j
-- Mathlib.Order.Partition.Basic
Partition.partscopyEquiv_apply_coe : ∀ {α : Type u_1} {s t : α} [inst : CompleteLattice α] (P : Partition s) (hst : s = t)
  (a : { a // (fun x => x ∈ ↑(P.copy hst)) a }), ↑((P.partscopyEquiv hst) a) = ↑a
-- Mathlib.Data.W.Cardinal
/-- If, for any `a : α`, `β a` is finite, then the cardinality of `WType β`
is at most the maximum of the cardinality of `α` and `ℵ₀`  -/
WType.cardinalMk_le_max_aleph0_of_finite' : ∀ {α : Type u} {β : α → Type v} [∀ (a : α), Finite (β a)],
  Cardinal.mk (WType β) ≤ max (Cardinal.lift.{v, u} (Cardinal.mk α)) Cardinal.aleph0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.empty_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp}, ∅ = t ↔ t = ∅
-- Init.Data.Nat.Bitwise.Lemmas
Nat.mod_two_eq_zero_iff_testBit_zero : ∀ {x : ℕ}, x % 2 = 0 ↔ x.testBit 0 = false
-- Lean.Meta.Sym.SymM
/-- Applies hash-consing to `e`. Recall that all expressions in a `grind` goal have
been hash-consed. We perform this step before we internalize expressions.

Depending on the current configuration, this function also maintains the `SymM`
invariants that reducible constants have been unfolded and kernel projections folded.
The checks are node-local and are only performed on terms that have not been
hash-consed before, so already-shared subterms cost nothing. When a violation is
found, the term is repaired using `unfoldReducible`/`foldProjs` and re-processed.
 -/
Lean.Meta.Sym.shareCommon : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instTrivialStar : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : CommSemiring R] [inst_4 : IsTopologicalSemiring R] [inst_5 : StarRing R] [inst_6 : ContinuousStar R]
  [TrivialStar R], TrivialStar (ContinuousMapZero X R)
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The functor which sends `X, Y` to the product type `X × Y`.  -/
CategoryTheory.Limits.Types.binaryProductFunctor : CategoryTheory.Functor (Type u) (CategoryTheory.Functor (Type u) (Type u))
-- Mathlib.Analysis.Complex.Norm
Complex.limAux.eq_1 : ∀ (f : CauSeq ℂ fun x => ‖x‖), Complex.limAux f = { re := (Complex.cauSeqRe f).lim, im := (Complex.cauSeqIm f).lim }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).maxKey?.isSome = true
-- Mathlib.GroupTheory.Perm.Basic
Set.BijOn.perm_zpow : ∀ {α : Type u_1} {f : Equiv.Perm α} {s : Set α}, Set.BijOn (⇑f) s s → ∀ (n : ℤ), Set.BijOn (⇑(f ^ n)) s s
-- Lean.Elab.DocString
Lean.Doc.Context.mk.sizeOf_spec : ∀ (suggestionMode : Lean.Doc.SuggestionMode), sizeOf { suggestionMode := suggestionMode } = 1 + sizeOf suggestionMode
-- Lean.DocString.Parser
/-- Finds the minimum column of the first non-whitespace character on each non-empty content line
between `startPos` and `endPos`, returning `init` if no such line exists.
 -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.minContentIndent : Lean.FileMap → String.Pos.Raw → String.Pos.Raw → ℕ → ℕ
-- Mathlib.RingTheory.Finiteness.Finsupp
LinearMap.finsuppLinearMap_injective : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (S : Type u_5) [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : Semiring S] [inst_6 : Module S N] [inst_7 : SMulCommClass R S N],
  Function.Injective ⇑(LinearMap.finsuppLinearMap S)
-- Mathlib.CategoryTheory.Linear.FunctorCategory
CategoryTheory.functorCategoryLinear : {R : Type u_1} →
  [inst : Semiring R] →
    {C : Type u_2} →
      {D : Type u_3} →
        [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
          [inst_2 : CategoryTheory.Category.{v_2, u_3} D] →
            [inst_3 : CategoryTheory.Preadditive D] →
              [CategoryTheory.Linear R D] → CategoryTheory.Linear R (CategoryTheory.Functor C D)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_inter_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ((t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂)
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.δ_μ : ∀ {G : Type v} [inst : Monoid G] (X Y : Action (Type w) G) {k : Type u} [inst_1 : CommSemiring k],
  (Representation.LinearizeMonoidal.δ X Y).comp (Representation.LinearizeMonoidal.μ X Y) =
    Representation.IntertwiningMap.id ((Representation.linearize k G X).tprod (Representation.linearize k G Y))
-- Lean.Parser.Basic
Lean.Parser.PrattParsingTables.leadingTable : Lean.Parser.PrattParsingTables → Lean.Parser.TokenMap (Lean.Parser.Parser × ℕ)
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.toLawfulOrderBEq : ∀ {α : Type u} [self : Std.PreorderPackage α], Std.LawfulOrderBEq α
-- Mathlib.Topology.Order.ScottTopology
Topology.scottHausdorff_le_scott : ∀ {α : Type u_1} [inst : Preorder α], Topology.scottHausdorff α Set.univ ≤ Topology.scott α Set.univ
-- Init.Data.Function
/-- `HasLeftInverse f` means that `f` has an unspecified left inverse.  -/
Function.HasLeftInverse : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Prop
-- Mathlib.LinearAlgebra.Basis.Defs
/-- Construct a linear map given the value at the basis, called `Basis.constr b S f` where `b` is
a basis, `f` is the value of the linear map over the elements of the basis, and `S` is an
extra semiring (typically `S = R` or `S = ℕ`).

This definition is parameterized over an extra `Semiring S`,
such that `SMulCommClass R S M'` holds.
If `R` is commutative, you can set `S := R`; if `R` is not commutative,
you can recover an `AddEquiv` by setting `S := ℕ`.
See library note [bundled maps over different rings].
 -/
Module.Basis.constr : {M' : Type u_7} →
  [inst : AddCommMonoid M'] →
    {ι : Type u_10} →
      {R : Type u_11} →
        {M : Type u_12} →
          [inst_1 : Semiring R] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] →
                Module.Basis ι R M →
                  [inst_4 : Module R M'] →
                    (S : Type u_13) →
                      [inst_5 : Semiring S] →
                        [inst_6 : Module S M'] → [inst_7 : SMulCommClass R S M'] → (ι → M') ≃ₗ[S] M →ₗ[R] M'
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.join₂_map : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R),
  MvPolynomial.join₂ ((MvPolynomial.map f) φ) = (MvPolynomial.bind₂ f) φ
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle**: if `f : E → F` is complex differentiable in a neighborhood of `c`
and the norm `‖f z‖` has a local maximum at `c`, then `‖f z‖` is locally constant in a neighborhood
of `c`.  -/
Complex.norm_eventually_eq_of_isLocalMax : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {c : E},
  (∀ᶠ (z : E) in nhds c, DifferentiableAt ℂ f z) → IsLocalMax (norm ∘ f) c → ∀ᶠ (y : E) in nhds c, ‖f y‖ = ‖f c‖
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.zsmul_zero' : ∀ {R : Type u} [self : AddGroupWithOne R] (a : R), 0 • a = 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postAdjunctionLeft_counit_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} {F : CategoryTheory.Functor T D} {G : CategoryTheory.Functor D T} (a : F ⊣ G)
  (A : CategoryTheory.Under (F.obj ((CategoryTheory.Functor.id T).obj X))),
  (CategoryTheory.Under.postAdjunctionLeft a).counit.app A = CategoryTheory.Under.homMk (a.counit.app A.right) ⋯
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mem_toSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Subsemiring R} {x : R}, x ∈ s.toSubmonoid ↔ x ∈ s
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.map : {β : Type u_1} →
  {G : Type u_2} →
    {α : Type u_3} → {inst : Monoid G} → {inst_1 : AddMonoid α} → [self : SlashAction β G α] → β → G → α → α
-- Lean.Util.ShareCommon
Lean.ShareCommon.persistentObjectFactory : ShareCommon.StateFactory
-- Init.Data.SInt.Bitwise
Int8.ofBitVec_or : ∀ (a b : BitVec 8), Int8.ofBitVec (a ||| b) = Int8.ofBitVec a ||| Int8.ofBitVec b
-- Init.Data.SInt.Bitwise
Int32.or_self : ∀ {a : Int32}, a ||| a = a
-- Mathlib.Topology.Filter
Filter.nhds_atBot : ∀ {α : Type u_2} [inst : Preorder α], nhds Filter.atBot = ⨅ x, Filter.principal (Set.Iic (Filter.principal (Set.Iic x)))
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion : ∀ {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C),
  (↑J).PairwiseDisjoint (hC.disjointOfUnion hJ)
-- Mathlib.Topology.DiscreteQuotient
/-- **Alias** of `DiscreteQuotient.isOpen_setOfPred_rel`.

---

For every point `x`, the set `{ y | Rel x y }` is an open set.  -/
DiscreteQuotient.isOpen_setOf_rel : ∀ {X : Type u_5} [inst : TopologicalSpace X] (self : DiscreteQuotient X) (x : X), IsOpen (Set.ofPred (self.toSetoid x))
-- Std.Data.String.ToInt
String.Slice.isInt_of_isNat : ∀ {s : String.Slice}, s.isNat = true → s.isInt = true
-- Mathlib.RingTheory.Discriminant
/-- The discriminant of a power basis.  -/
Algebra.discr_powerBasis_eq_prod : ∀ (K : Type u) {L : Type v} (E : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Field E] [inst_3 : Algebra K L]
  [inst_4 : Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) (e : Fin pb.dim ≃ (L →ₐ[K] E))
  [Algebra.IsSeparable K L],
  (algebraMap K E) (Algebra.discr K ⇑pb.basis) = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
CategoryTheory.CommSq.LiftStruct.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (l l_1 : B ⟶ X) (e_l : l = l_1)
  (fac_left : CategoryTheory.CategoryStruct.comp i l = f) (fac_right : CategoryTheory.CategoryStruct.comp l p = g),
  { l := l, fac_left := fac_left, fac_right := fac_right } = { l := l_1, fac_left := ⋯, fac_right := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k k' fallback : α},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).getKeyD k' fallback = k
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- A structure expressing that `X : C` is the limit of a functor
`diag : J ⥤ C` such that `P (diag.obj j)` holds for all `j`.  -/
CategoryTheory.ObjectProperty.LimitOfShape : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C →
      (J : Type u') → [CategoryTheory.Category.{v', u'} J] → C → Type (max (max (max u' u_1) v') v_1)
-- Lean.Data.Lsp.Internal
/-- Results for each query in `LeanQueryModuleParams`.
Positions correspond to `queries` in the parameter of the request.
 -/
Lean.Lsp.LeanQueryModuleResponse.queryResults : Lean.Lsp.LeanQueryModuleResponse → Array Lean.Lsp.LeanQueriedModule
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.L1.integral_of_fun_eq_integral' : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G} (hf : MeasureTheory.Integrable f μ),
  ∫ (a : α), ↑(MeasureTheory.AEEqFun.mk f ⋯) a ∂μ = ∫ (a : α), f a ∂μ
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.codRestrict_apply_coe : ∀ {M : Type u_1} {N : Type u_2} {σ : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : SetLike σ N]
  [inst_3 : MulMemClass σ N] (f : M →ₙ* N) (S : σ) (h : ∀ (x : M), f x ∈ S) (n : M), ↑((f.codRestrict S h) n) = f n
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.comap_map_eq : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (p : Submodule R M),
  Submodule.comap f (Submodule.map f p) = p ⊔ f.ker
-- Mathlib.Data.Fin.Pigeonhole
/-- If we have an injective map from `Fin m` to `Fin n`, then `m ≤ n`.
See also `Fintype.card_le_of_injective` for the generalisation to arbitrary finite types.
 -/
Fin.le_of_injective : ∀ {m n : ℕ} (f : Fin m → Fin n), Function.Injective f → m ≤ n
-- Lean.Structure
Lean.instInhabitedStructureResolutionOrderResult : Inhabited Lean.StructureResolutionOrderResult
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerveMap_app_mk₁ : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  (F : CategoryTheory.Functor C D) {x y : C} (f : x ⟶ y),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.nerveMap F).app (Opposite.op { len := 1 })))
      (CategoryTheory.ComposableArrows.mk₁ f) =
    CategoryTheory.ComposableArrows.mk₁ (F.map f)
-- Mathlib.Order.Concept
extentClosure_apply : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (x : Set α), (extentClosure r) x = lowerPolar r (upperPolar r x)
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso'_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C}
  (t : CategoryTheory.Limits.IsTerminal T),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso' X i t).inv.right =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right
        (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.hasMFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {s : Set H}
  {x : H}, HasMFDerivAt[s] (↑I) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearMap.codRestrict₂_apply : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Module R M] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module R M₃] (f : M₁ →ₗ[R] M₂ →ₗ[R] M)
  (i : M₃ →ₗ[R] M) (hi : Function.Injective ⇑i) (hf : ∀ (x : M₁) (y : M₂), (f x) y ∈ i.range) (x : M₁) (y : M₂),
  i (((f.codRestrict₂ i hi hf) x) y) = (f x) y
-- Mathlib.Analysis.Matrix.Hermitian
Matrix.isHermitian_iff_isSymmetric : ∀ {𝕜 : Type u_1} {n : Type u_3} {A : Matrix n n 𝕜} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  A.IsHermitian ↔ (Matrix.toEuclideanLin A).IsSymmetric
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv_symm_monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (r : Rᵐᵒᵖ),
  (Polynomial.opRingEquiv R).symm ((Polynomial.monomial n) r) =
    MulOpposite.op ((Polynomial.monomial n) (MulOpposite.unop r))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_union : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k)
-- Mathlib.Data.Finset.Interval
/-- Cardinality of an `Ioc` of finsets.  -/
Finset.card_Ioc_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊆ t → (Finset.Ioc s t).card = 2 ^ (t.card - s.card) - 1
-- Mathlib.Order.Radical
OrderIso.map_radical : ∀ {α : Type u_1} [inst : CompleteLattice α] {β : Type u_2} [inst_1 : CompleteLattice β] (f : α ≃o β),
  f (Order.radical α) = Order.radical β
-- Mathlib.Data.List.Rotate
/-- `IsRotated l₁ l₂` or `l₁ ~r l₂` asserts that `l₁` and `l₂` are cyclic permutations
of each other. This is defined by claiming that `∃ n, l.rotate n = l'`.  -/
List.«term_~r_» : Lean.TrailingParserDescr
-- Std.Internal.Do.ExceptPost
/-- The head exception postcondition.  -/
Std.Internal.Do.EPost.Cons.head : {eh : Type u} → {et : Type v} → EPost.Cons✝ eh et → eh