mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.mk.injEq : ∀
  (userTime systemTime maxRSS ixRSS idRSS isRSS minFlt majFlt nSwap inBlock outBlock msgSent msgRecv signals voluntaryCS
    involuntaryCS userTime_1 systemTime_1 maxRSS_1 ixRSS_1 idRSS_1 isRSS_1 minFlt_1 majFlt_1 nSwap_1 inBlock_1
    outBlock_1 msgSent_1 msgRecv_1 signals_1 voluntaryCS_1 involuntaryCS_1 : UInt64),
  ({ userTime := userTime, systemTime := systemTime, maxRSS := maxRSS, ixRSS := ixRSS, idRSS := idRSS, isRSS := isRSS,
        minFlt := minFlt, majFlt := majFlt, nSwap := nSwap, inBlock := inBlock, outBlock := outBlock,
        msgSent := msgSent, msgRecv := msgRecv, signals := signals, voluntaryCS := voluntaryCS,
        involuntaryCS := involuntaryCS } =
      { userTime := userTime_1, systemTime := systemTime_1, maxRSS := maxRSS_1, ixRSS := ixRSS_1, idRSS := idRSS_1,
        isRSS := isRSS_1, minFlt := minFlt_1, majFlt := majFlt_1, nSwap := nSwap_1, inBlock := inBlock_1,
        outBlock := outBlock_1, msgSent := msgSent_1, msgRecv := msgRecv_1, signals := signals_1,
        voluntaryCS := voluntaryCS_1, involuntaryCS := involuntaryCS_1 }) =
    (userTime = userTime_1 ∧
      systemTime = systemTime_1 ∧
        maxRSS = maxRSS_1 ∧
          ixRSS = ixRSS_1 ∧
            idRSS = idRSS_1 ∧
              isRSS = isRSS_1 ∧
                minFlt = minFlt_1 ∧
                  majFlt = majFlt_1 ∧
                    nSwap = nSwap_1 ∧
                      inBlock = inBlock_1 ∧
                        outBlock = outBlock_1 ∧
                          msgSent = msgSent_1 ∧
                            msgRecv = msgRecv_1 ∧
                              signals = signals_1 ∧ voluntaryCS = voluntaryCS_1 ∧ involuntaryCS = involuntaryCS_1)
-- Mathlib.Data.Nat.Factorization.LCM
Nat.factorizationLCMLeft_zero_left : ∀ (b : ℕ), Nat.factorizationLCMLeft 0 b = 1
-- Mathlib.Order.WithBot
WithTop.map_ofDual : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : WithTop αᵒᵈ),
  WithTop.map f (WithTop.ofDual a) = WithTop.map (⇑OrderDual.ofDual ∘ f) a
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.instIsRightAdjointCommRingCatOppositeLocallyRingedSpaceΓ : AlgebraicGeometry.LocallyRingedSpace.Γ.IsRightAdjoint
-- Init.Data.String.Pattern.Char
String.Slice.Pattern.Char.instForwardPatternChar : {c : Char} → String.Slice.Pattern.ForwardPattern c
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.normalizePublishDiagnosticsParams : Lean.Lsp.PublishDiagnosticsParams → Lean.Lsp.PublishDiagnosticsParams
-- Mathlib.Data.List.Sort
StrictMono.sortedLT_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {l : List α},
  StrictMono f → ((List.map f l).SortedLT ↔ l.SortedLT)
-- Init.Data.Fin.Lemmas
Fin.succ_ne_zero : ∀ {n : ℕ} (k : Fin n), k.succ ≠ 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- For an open immersion `f : X ⟶ Y` and an open set `U ⊆ X`, we have the map `X(U) ⟶ Y(U)`.  -/
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f : X ⟶ Y) →
    [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f] →
      (U : TopologicalSpace.Opens ↑X.toTopCat) →
        X.presheaf.obj (Opposite.op U) ⟶
          Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj U))
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_bot_left : ∀ {Ω : Type u_1} (m₁ : MeasurableSpace Ω) {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ], ProbabilityTheory.CondIndep m' ⊥ m₁ hm' μ
-- Mathlib.Algebra.Category.Grp.Colimits
/-- The category of additive commutative groups has all small colimits.
 -/
AddCommGrpCat.hasColimitsOfSize : ∀ [UnivLE.{u, w}], CategoryTheory.Limits.HasColimitsOfSize.{v, u, w, w + 1} AddCommGrpCat
-- Mathlib.RingTheory.Perfection
Perfection.coeff_mapMonoidHom : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {M : Type u_1} {N : Type u_2} [inst_1 : CommMonoid M] [inst_2 : CommRing N]
  [inst_3 : CharP N p] (e : M →* N) (n : ℕ) (x : Perfection M p),
  (Perfection.coeff N p n) ((Perfection.mapMonoidHom p e) x) = e ((Perfection.coeffMonoidHom M p n) x)
-- Mathlib.Algebra.Algebra.Defs
/-- The canonical ring homomorphism `algebraMap R A : R →+* A` for any `R`-algebra `A`,
packaged as an `R`-linear map.
 -/
RingTheory.LinearMap.termη : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.exp_four_lt : Real.exp 4 < 64
-- Mathlib.Analysis.Convolution
/-- Convolution is associative. This has a weak but inconvenient integrability condition.
See also `MeasureTheory.convolution_assoc`.  -/
MeasureTheory.convolution_assoc' : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF} {F' : Type uF'}
  {F'' : Type uF''} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup E'']
  [inst_3 : NormedAddCommGroup F] {f : G → E} {g : G → E'} [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedSpace 𝕜 E'] [inst_7 : NormedSpace 𝕜 E''] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedSpace 𝕜 F]
  [inst_10 : MeasurableSpace G] {μ ν : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [CompleteSpace F]
  [inst_12 : NormedAddCommGroup F'] [inst_13 : NormedSpace ℝ F'] [inst_14 : NormedSpace 𝕜 F'] [CompleteSpace F']
  [inst_16 : NormedAddCommGroup F''] [inst_17 : NormedSpace ℝ F''] [inst_18 : NormedSpace 𝕜 F''] [CompleteSpace F'']
  {k : G → E''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'')
  [inst_20 : AddGroup G] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [μ.IsAddRightInvariant] [MeasurableAdd₂ G]
  [ν.IsAddRightInvariant] [MeasurableNeg G],
  (∀ (x : E) (y : E') (z : E''), (L₂ (⋯ y)) z = (L₃ x) ((L₄ y) z)) →
    ∀ {x₀ : G},
      (∀ᵐ (y : G) ∂μ, MeasureTheory.ConvolutionExistsAt f g y L ν) →
        (∀ᵐ (x : G) ∂ν, MeasureTheory.ConvolutionExistsAt g k x L₄ μ) →
          MeasureTheory.Integrable (Function.uncurry fun x y => ⋯) (μ.prod ν) →
            MeasureTheory.convolution (MeasureTheory.convolution f g L ν) k L₂ μ x₀ =
              MeasureTheory.convolution f (MeasureTheory.convolution g k L₄ μ) L₃ ν x₀
-- Mathlib.Data.Multiset.Sum
Multiset.disjSum_strictMono_left : ∀ {α : Type u_1} {β : Type u_2} (t : Multiset β), StrictMono fun s => s.disjSum t
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensorRightTensor_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategory.tensorRightTensor X Y).hom.app Z =
    (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_inj : ∀ {α : Type u_1} {a b : αˢʸᵐ}, SymAlg.unsym a = SymAlg.unsym b ↔ a = b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula.0.tacticEval_simp : Lean.ParserDescr
-- Mathlib.Data.Finset.Image
Finset.map_cast_heq : ∀ {α β : Type u_4} (h : α = β) (s : Finset α), Finset.map (Equiv.cast h).toEmbedding s ≍ s
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.map_mul : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (a b : M), f (a * b) = f a * f b
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.injective_of_iterate_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f' : Module.End R M} {n : ℕ}, n ≠ 0 → Function.Injective ⇑(f' ^ n) → Function.Injective ⇑f'
-- Mathlib.Data.List.Perm.Basic
List.Perm.product : ∀ {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {t₁ t₂ : List β},
  l₁.Perm l₂ → t₁.Perm t₂ → (l₁.product t₁).Perm (l₂.product t₂)
-- Mathlib.Data.Set.Pairwise.Chain
IsChain.pairwiseDisjoint_iUnion₂ : ∀ {α : Type u_1} {β : Type u_2} {c : Set (Set α)},
  IsChain (fun x1 x2 => x1 ⊆ x2) c →
    ∀ [inst : PartialOrder β] [inst_1 : OrderBot β] (f : α → β),
      (⋃ s ∈ c, s).PairwiseDisjoint f ↔ ∀ s ∈ c, s.PairwiseDisjoint f
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.map : ∀ {α β : Type u_1} {s : Set α} (f : α → β), s.Finite → (f <$> s).Finite
-- Mathlib.Data.List.InsertIdx
List.insertIdx_pmap : ∀ {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} {a : α} {n : ℕ} (hl : ∀ x ∈ l, p x)
  (ha : p a), (List.pmap f l hl).insertIdx n (f a ha) = List.pmap f (l.insertIdx n a) ⋯
-- Mathlib.Algebra.Quaternion
Quaternion.imK_one : ∀ {R : Type u_3} [inst : CommRing R], QuaternionAlgebra.imK 1 = 0
-- Mathlib.Topology.Order.Bornology
IsOrderBornology.atTop_le_cobounded : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α] [NoMaxOrder α],
  Filter.atTop ≤ Bornology.cobounded α
-- Std.Sat.AIG.Basic
/-- Flip the polarity of `Ref`.
 -/
Std.Sat.AIG.Ref.not : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.Ref → aig.Ref
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `Matrix.mulVec` as a bilinear map.

When `A` is non-commutative, this can be instantiated as `mulVecBilin A Aᵐᵒᵖ`  -/
Matrix.mulVecBilin : {m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_4) →
      (S : Type u_5) →
        {A : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : Module R A] →
                  [inst_4 : Module S A] →
                    [inst_5 : SMulCommClass S R A] →
                      [SMulCommClass S A A] →
                        [IsScalarTower R A A] → [Fintype n] → Matrix m n A →ₗ[R] (n → A) →ₗ[S] m → A
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The notation `\textf` for `WeierstrassCurve.Projective.baseChange W S`.  -/
WeierstrassCurve.Projective.«term_⁄_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- A functor `G : (C, J) ⥤ (D, K)` is cover dense if for each object in `D`,
there exists a covering sieve in `D` that factors through images of `G`.

This definition can be found in https://ncatlab.org/nlab/show/dense+sub-site Definition 2.2.
 -/
CategoryTheory.Functor.IsCoverDense : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor C D → CategoryTheory.GrothendieckTopology D → Prop
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Verify that replacing `grind` with `grind?` produces a valid `grind only` suggestion.  -/
linter.tacticAnalysis.verifyGrindOnly : Lean.Option Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.op_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Fork f g)
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  c.op.ι.app X_1 =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.parallelPairOpIso f g).hom.app X_1)
      (c.π.app (Opposite.unop (CategoryTheory.Limits.walkingParallelPairOp.obj X_1))).op
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.induction_on₂ : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Localization S → Prop}
  (x y : Localization S), (∀ (x y : M × ↥S), p (Localization.mk x.1 x.2) (Localization.mk y.1 y.2)) → p x y
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.includeLeft_surjective : ∀ {R : Type u_1} {T : Type u_4} [inst : CommSemiring R] [inst_1 : Ring T] [inst_2 : Algebra R T] (S : Type u_5)
  (A : Type u_6) [inst_3 : CommSemiring S] [inst_4 : Semiring A] [inst_5 : Algebra S A] [inst_6 : Algebra R A]
  [inst_7 : SMulCommClass R S A],
  Function.Surjective ⇑(algebraMap R T) → Function.Surjective ⇑Algebra.TensorProduct.includeLeft
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.coyonedaPreservesLimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : Type w) [inst_1 : CategoryTheory.Category.{t, w} J]
  (X : Cᵒᵖ), CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.coyoneda.obj X)
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.OrderType.lin : Mathlib.Tactic.Order.OrderType
-- Mathlib.Topology.Order.ScottTopology
Topology.scottHausdorff_le_lower : ∀ {α : Type u_1} [inst : Preorder α], Topology.scottHausdorff α Set.univ ≤ Topology.lower α
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Shannon q-ary Entropy function (measured in Nats, i.e., using natural logs).

It's the Shannon entropy of a random variable with possible outcomes `{1, ..., q}`
where outcome `1` has probability `1 - p` and all other outcomes are equally likely.

The usual domain of definition is `p ∈ [0,1]`, i.e., input is a probability.

This is a generalization of the binary entropy function `binEntropy`.  -/
Real.qaryEntropy : ℕ → ℝ → ℝ
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationParams.expr : ProofWidgets.GetExprPresentationParams → Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx
-- Mathlib.Analysis.Calculus.Deriv.Inv
deriv_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜}, deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.coe_deriv₂ : ∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Fₗ] [inst_2 : SeminormedAddCommGroup Gₗ] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace 𝕜 Gₗ] (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ)
  (p : E × Fₗ), ⇑(f.deriv₂ p) = fun q => (f p.1) q.2 + (f q.1) p.2
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.isMissingDoc : Lean.Syntax → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.NumberTheory.FLT.Polynomial
Polynomial.flt : ∀ {k : Type u_1} [inst : Field k] {n : ℕ},
  3 ≤ n →
    ↑n ≠ 0 →
      ∀ {a b c : Polynomial k},
        a ≠ 0 →
          b ≠ 0 → c ≠ 0 → IsCoprime a b → a ^ n + b ^ n = c ^ n → a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonAssocSemiring α] [inst_1 : Preorder α]
  [inst_2 : NonAssocSemiring β] [inst_3 : Preorder β] [inst_4 : NonAssocSemiring γ] [inst_5 : Preorder γ] (f : β →+*o γ)
  (g : α →+*o β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.eq_liftHomotopy_iff' : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) {H : C(↑unitInterval × A, X)} {f : C(A, E)}
  (H_0 : ∀ (a : A), H (0, a) = p (f a)) (H' : C(↑unitInterval × A, E)),
  H' = cov.liftHomotopy H f H_0 ↔ p ∘ ⇑H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
left Kan extension at `Y` iff `E'` is.  -/
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIso : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E E' : L.LeftExtension F} →
                  (E ≅ E') → (Y : D) → E.IsPointwiseLeftKanExtensionAt Y ≃ E'.IsPointwiseLeftKanExtensionAt Y
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [toHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms C] →
      [toIsNormalMonoCategory : CategoryTheory.IsNormalMonoCategory C] →
        [toIsNormalEpiCategory : CategoryTheory.IsNormalEpiCategory C] →
          [has_zero_object : CategoryTheory.Limits.HasZeroObject C] →
            [has_kernels : CategoryTheory.Limits.HasKernels C] →
              [has_cokernels : CategoryTheory.Limits.HasCokernels C] →
                [has_finite_products : CategoryTheory.Limits.HasFiniteProducts C] →
                  [has_finite_coproducts : CategoryTheory.Limits.HasFiniteCoproducts C] →
                    CategoryTheory.NonPreadditiveAbelian C
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.srange_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M → N) (hf : ∀ (x y : M), f (x + y) = f x + f y),
  { toFun := f, map_add' := hf }.srange = { carrier := Set.range f, add_mem' := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.instModuleCarrierObjOppositeCommRingCatCarrierCarrierRingCatCompForget₂RingHomObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
      (X : Cᵒᵖ) →
        (M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) → Module ↑(R.obj X) ↑(M.obj X)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instAddMonoid : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] →
                        [inst_7 : Module R₂ M₂] → [ContinuousAdd M₂] → AddMonoid (M₁ →SL[σ₁₂] M₂)
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Pos.find?_char_eq_none_iff_not_mem_of_splits : ∀ {c : Char} {s : String} {pos : s.Pos} {t u : String}, pos.Splits t u → (pos.find? c = none ↔ c ∉ u.toList)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.transitionMap_map_pow : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {m n a : ℕ} (hmn : m ≤ n) (x : R ⧸ I ^ n • ⊤),
  (AdicCompletion.transitionMap I R hmn) (x ^ a) = (AdicCompletion.transitionMap I R hmn) x ^ a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β k}, a ∈ m.insert k v → (k == a) = false → a ∈ m
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj₂.isAssociative_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [Std.Associative ga],
  Function.Semiconj₂ f ga gb → Function.Surjective f → Std.Associative gb
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.hom_comp : ∀ {R : Type u} [inst : CommRing R] {A B C : CommBialgCat R} (f : A ⟶ B) (g : B ⟶ C),
  CommBialgCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (CommBialgCat.Hom.hom g).comp (CommBialgCat.Hom.hom f)
-- Mathlib.Computability.Primrec.Basic
PrimrecRel.of_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {r s : α → β → Prop},
  PrimrecRel r → (∀ (a : α) (b : β), r a b ↔ s a b) → PrimrecRel s
-- Mathlib.Control.Bifunctor
Bifunctor.snd_comp_snd : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β₀ β₁ β₂ : Type u₁}
  (g : β₀ → β₁) (g' : β₁ → β₂), Bifunctor.snd g' ∘ Bifunctor.snd g = Bifunctor.snd (g' ∘ g)
-- Init.Data.List.Sublist
List.infix_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, l <:+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a
-- Mathlib.Data.Finset.Card
Finset.card_image_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [inst : DecidableEq β],
  (Finset.image f s).card = s.card ↔ Set.InjOn f ↑s
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.roots_charpoly_eq_eigenvalues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n),
  T.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hT.eigenvalues hn) Finset.univ.val
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.gt_of_tendsto_zero_of_neg : ∀ {f : ℕ → ℝ}, Filter.Tendsto f Filter.atTop (nhds 0) → ∀ {r : ℝ}, r < 0 → ↑r < Hyperreal.ofSeq f
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.wellFoundedOn : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsPreorder α r],
  s.PartiallyWellOrderedOn r → s.WellFoundedOn fun a b => r a b ∧ ¬r b a
-- Lean.Message
Lean.instInhabitedBaseMessage : {a : Type u_1} → [Inhabited a] → Inhabited (Lean.BaseMessage a)
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isAffineHom_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsAffineHom f ↔
    ∀ (U : Y.Opens),
      AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Cache.WF.below.empty : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α]
  {motive :
    (a : Array (Std.Sat.AIG.Decl α)) → (a_1 : Std.HashMap (Std.Sat.AIG.Decl α) ℕ) → Std.Sat.AIG.Cache.WF a a_1 → Prop}
  {decls : Array (Std.Sat.AIG.Decl α)}, Std.Sat.AIG.Cache.WF.below ⋯
-- Mathlib.LinearAlgebra.Prod
Submodule.snd.eq_1 : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], Submodule.snd R M M₂ = Submodule.comap (LinearMap.fst R M M₂) ⊥
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instModuleFinite : ∀ (R : Type u_1) (A : Type u_3) (E : Type u_4) [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [Module.Finite R E], Module.Finite R (WithCStarModule A E)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Mathlib.Order.ConditionallyCompleteLattice.Group
ciSup_mul_le_ciSup_mul_ciSup : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Mul α] [MulLeftMono α]
  [MulRightMono α] {f g : ι → α},
  BddAbove (Set.range f) → BddAbove (Set.range g) → ⨆ i, f i * g i ≤ (⨆ i, f i) * ⨆ i, g i
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mul_lt_aleph0_iff_of_ne_zero : ∀ {a b : Cardinal.{u_1}}, a ≠ 0 → b ≠ 0 → (a * b < Cardinal.aleph0 ↔ a < Cardinal.aleph0 ∧ b < Cardinal.aleph0)
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `s₁` and `s₂` be two `R`-algebra isomorphisms. Then `s₂ x` is a conjugate root of `s₁ x`.
 -/
isConjRoot_of_algEquiv₂ : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A)
  (s₁ s₂ : A ≃ₐ[R] A), IsConjRoot R (s₁ x) (s₂ x)
-- Aesop.Index.Basic
Aesop.IndexingMode.targetMatchingConclusion : Lean.Expr → Lean.MetaM Aesop.IndexingMode
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₇ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] →
      Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Data.Erased
/-- Extracts the erased value, noncomputably.  -/
Erased.out : {α : Sort u_1} → Erased α → α
-- Std.Http.Server.Config
/-- Maximum number of simultaneous active connections (default: 1024).
Setting this to `0` disables the limit entirely: the server will accept any number of
concurrent connections and no semaphore-based cap is enforced. Use with care — an
unconstrained server may exhaust file descriptors or memory under adversarial load.
 -/
Std.Http.Config.maxConnections : Std.Http.Config → ℕ