mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Defs
String.utf8EncodeChar.eq_def : ∀ (c : Char),
  String.utf8EncodeChar c =
    have v := c.val.toNat;
    if v ≤ 127 then [UInt8.ofNat v]
    else
      if v ≤ 2047 then [UInt8.ofNat (v / 64 % 32 + 192), UInt8.ofNat (v % 64 + 128)]
      else
        if v ≤ 65535 then
          [UInt8.ofNat (v / 4096 % 16 + 224), UInt8.ofNat (v / 64 % 64 + 128), UInt8.ofNat (v % 64 + 128)]
        else
          [UInt8.ofNat (v / 262144 % 8 + 240), UInt8.ofNat (v / 4096 % 64 + 128), UInt8.ofNat (v / 64 % 64 + 128),
            UInt8.ofNat (v % 64 + 128)]
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_smul : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : αᵒᵈ), OrderDual.ofDual (b • a) = b • OrderDual.ofDual a
-- Mathlib.Data.List.NodupEquivFin
List.getEquivOfForallCountEqOne_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : ∀ (x : α), List.count x l = 1) (i : Fin l.length),
  (l.getEquivOfForallCountEqOne h) i = l[↑i]
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.one_le_prod_of_one_le : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] {s : Multiset α} [MulLeftMono α],
  (∀ x ∈ s, 1 ≤ x) → 1 ≤ s.prod
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.jmp.injEq : ∀ (j : Lean.IR.JoinPointId) (ys : Array Lean.IR.Arg) (j_1 : Lean.IR.JoinPointId) (ys_1 : Array Lean.IR.Arg),
  (Lean.IR.FnBody.jmp j ys = Lean.IR.FnBody.jmp j_1 ys_1) = (j = j_1 ∧ ys = ys_1)
-- Mathlib.Analysis.Analytic.Constructions
/-- Multiplication in a normed algebra over `𝕜` is analytic.  -/
analyticAt_mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {A : Type u_7} [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  (z : A × A), AnalyticAt 𝕜 (fun x => x.1 * x.2) z
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instCommSemiring : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [CommSemiring β] → CommSemiring (MeasureTheory.SimpleFunc α β)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k},
  (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instInhabited : {α : Type u} → {cmp : α → α → Ordering} → Inhabited (Std.ExtTreeSet α cmp)
-- Lean.Declaration
Lean.TheoremVal.mk : Lean.ConstantVal → Lean.Expr → List Lean.Name → Lean.TheoremVal
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.Limits.FormalCoproduct C} → (f : X.I → Y.I) → ((i : X.I) → X.obj i ⟶ Y.obj (f i)) → X.Hom Y
-- Mathlib.Topology.Separation.Hausdorff
isClosed_diagonal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X], IsClosed (Set.diagonal X)
-- Mathlib.Analysis.Normed.Ring.Basic
RingHomIsometric.mk : ∀ {R₁ : Type u_5} {R₂ : Type u_6} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Norm R₁] [inst_3 : Norm R₂]
  {σ : R₁ →+* R₂}, (∀ {x : R₁}, ‖σ x‖ = ‖x‖) → RingHomIsometric σ
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.CommandCodeActionEntry.mk : Lean.Name → Array Lean.Name → Lean.CodeAction.CommandCodeActionEntry
-- Mathlib.NumberTheory.ModularForms.Basic
_private.Mathlib.NumberTheory.ModularForms.Basic.0.slash_J : ∀ (f : UpperHalfPlane → ℂ) (k : ℤ),
  SlashAction.map k UpperHalfPlane.J f = fun τ => (starRingEnd ℂ) (f (↑UpperHalfPlane.ofComplex (-(starRingEnd ℂ) ↑τ)))
-- Mathlib.Analysis.Normed.Group.Basic
norm_of_subsingleton' : ∀ {E : Type u_5} [inst : SeminormedGroup E] [Subsingleton E] (a : E), ‖a‖ = 0
-- Mathlib.Topology.Algebra.GroupWithZero
map_mul_right_nhds₀ : ∀ {G₀ : Type u_3} [inst : TopologicalSpace G₀] [inst_1 : GroupWithZero G₀] [SeparatelyContinuousMul G₀] {a : G₀},
  a ≠ 0 → ∀ (b : G₀), Filter.map (fun x => x * a) (nhds b) = nhds (b * a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_eq_getD : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {a : α} {fallback : β}, Std.DTreeMap.Internal.Impl.Const.getD t a fallback = t.getD a fallback
-- Mathlib.Algebra.Group.ULift
ULift.nontrivial : ∀ {α : Type u} [Nontrivial α], Nontrivial (ULift.{u_1, u} α)
-- Mathlib.CategoryTheory.CofilteredSystem
/-- The subfunctor of `F` obtained by restricting to the eventual range at each index.  -/
CategoryTheory.Functor.toEventualRanges : {J : Type u} →
  [inst : CategoryTheory.Category.{v_1, u} J] →
    CategoryTheory.Functor J (Type v) → [CategoryTheory.IsCofilteredOrEmpty J] → CategoryTheory.Functor J (Type v)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSumNat.add.inj : ∀ {a b : Q(ℕ)} {a_1 : Mathlib.Tactic.Ring.Common.ExProdNat a} {a_2 : Mathlib.Tactic.Ring.Common.ExSumNat b}
  {a_3 : Mathlib.Tactic.Ring.Common.ExProdNat a} {a_4 : Mathlib.Tactic.Ring.Common.ExSumNat b},
  Mathlib.Tactic.Ring.Common.ExSumNat.add a_1 a_2 = Mathlib.Tactic.Ring.Common.ExSumNat.add a_3 a_4 →
    a_1 = a_3 ∧ a_2 = a_4
-- Mathlib.RingTheory.Idempotents
instCommSemiringCorner : {R : Type u_1} → (e : R) → [inst : NonUnitalCommSemiring R] → (idem : IsIdempotentElem e) → CommSemiring idem.Corner
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (toStrictlyUnitaryPseudofunctor : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (map_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toStrictlyUnitaryPseudofunctor.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toStrictlyUnitaryPseudofunctor.map f)
            (toStrictlyUnitaryPseudofunctor.map g))
      CategoryTheory.StrictPseudofunctor.map_comp._autoParam)
  (mapComp_eq_eqToIso :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), toStrictlyUnitaryPseudofunctor.mapComp f g = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso._autoParam),
  sizeOf
      { toStrictlyUnitaryPseudofunctor := toStrictlyUnitaryPseudofunctor, map_comp := map_comp,
        mapComp_eq_eqToIso := mapComp_eq_eqToIso } =
    1 + sizeOf toStrictlyUnitaryPseudofunctor
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The property that a morphism between monoid objects is a monoid morphism.  -/
CategoryTheory.IsMonHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : C} → [CategoryTheory.MonObj M] → [CategoryTheory.MonObj N] → (M ⟶ N) → Prop
-- Batteries.Data.Fin.Basic
/-- Count the number of true values of a decidable predicate on `Fin n`.  -/
Fin.countP : {n : ℕ} → (Fin n → Bool) → ℕ
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Geometric progressions of length three are unchanged under `2`-Freiman isomorphisms.  -/
threeGPFree_image : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s A : Set α} {t : Set β} {f : α → β},
  IsMulFreimanIso 2 s t f → A ⊆ s → (ThreeGPFree (f '' A) ↔ ThreeGPFree A)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.hasOpNorm : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → [Fintype ι] → Norm (ContinuousMultilinearMap 𝕜 E G)
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.join.eq_1 : ∀ (l : List String.Slice), String.Slice.join l = List.foldl (fun r s => r ++ s) "" l
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.induction : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {motive : SymmetricAlgebra R M → Prop},
  (∀ (r : R), motive ((algebraMap R (SymmetricAlgebra R M)) r)) →
    (∀ (x : M), motive ((SymmetricAlgebra.ι R M) x)) →
      (∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a * b)) →
        (∀ (a b : SymmetricAlgebra R M), motive a → motive b → motive (a + b)) → ∀ (a : SymmetricAlgebra R M), motive a
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.splitAt : Lean.MVarId → Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.Topology.Connected.PathConnected
pathComponentIn_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F : Set X}, pathComponentIn F x ⊆ F
-- Init.Data.Nat.Lemmas
Nat.sub_add_min_cancel : ∀ (n m : ℕ), n - m + min n m = n
-- Mathlib.Data.Seq.Defs
Stream'.Seq.head_eq_destruct : ∀ {α : Type u} (s : Stream'.Seq α), s.head = Prod.fst <$> s.destruct
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.instMax : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → Max (HomogeneousIdeal 𝒜)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_finsetSum : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R),
  (s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddGroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α],
  OrderDual.instAddGroup = { toSubNegMonoid := OrderDual.instSubNegAddMonoid, neg_add_cancel := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.not_lt_iff : ∀ {w : ℕ} {b : BitVec w}, ~~~b < b ↔ 0 < w ∧ b.msb = true
-- Mathlib.Algebra.Group.Int.Even
Int.ediv_two_mul_two_of_even : ∀ {n : ℤ}, Even n → n / 2 * 2 = n
-- Mathlib.Topology.Connected.PathConnected
pathComponentIn_mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F G : Set X}, F ⊆ G → pathComponentIn F x ⊆ pathComponentIn G x
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.exists_pow_nat_eq : ∀ {k : Type u} [inst : Field k] [IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero ↑n], ∃ z, z ^ n = x
-- Mathlib.Data.Stream.Defs
/-- Given a stream of functions and a stream of values, apply `n`-th function to `n`-th value.  -/
Stream'.apply : {α : Type u} → {β : Type v} → Stream' (α → β) → Stream' α → Stream' β
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- Two `CliffordAlgebra`s are equivalent as algebras if their quadratic forms are
equivalent.  -/
CliffordAlgebra.equivOfIsometry : {R : Type u_1} →
  [inst : CommRing R] →
    {M₁ : Type u_4} →
      {M₂ : Type u_5} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {Q₁ : QuadraticForm R M₁} →
                  {Q₂ : QuadraticForm R M₂} →
                    QuadraticMap.IsometryEquiv Q₁ Q₂ → CliffordAlgebra Q₁ ≃ₐ[R] CliffordAlgebra Q₂
-- Mathlib.Condensed.Discrete.Module
/-- Auxiliary definition for `functorIsoDiscrete`.  -/
LightCondMod.LocallyConstant.functorIsoDiscreteComponents : (R : Type u) →
  [inst : Ring R] →
    (M : ModuleCat R) → (LightCondensed.discrete (ModuleCat R)).obj M ≅ (LightCondMod.LocallyConstant.functor R).obj M
-- Mathlib.Algebra.Order.Field.Basic
mul_sub_mul_div_mul_nonpos_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {a b c d : α},
  c ≠ 0 → d ≠ 0 → ((a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_mapPullbackAdj_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) (T : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)),
  (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).unit.app
      T =
    CategoryTheory.Over.homMk
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp T.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y))
        (CategoryTheory.CategoryStruct.id
          ((CategoryTheory.Functor.id (CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))).obj
              T).left))
      ⋯
-- Lean.Data.Lsp.Internal
Lean.Lsp.OpenNamespace.renamed.inj : ∀ {«from» «to» from_1 to_1 : Lean.Name},
  Lean.Lsp.OpenNamespace.renamed «from» «to» = Lean.Lsp.OpenNamespace.renamed from_1 to_1 →
    «from» = from_1 ∧ «to» = to_1
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.of_subsingleton : ∀ {V : Type u_1} [Subsingleton V] {G : SimpleGraph V}, G.IsAcyclic
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] (𝒰 : X.OpenCover),
  ⨅ i, AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) =
    AlgebraicGeometry.Scheme.Hom.ker f
-- Lean.Message
Lean.instToMessageDataExpr : Lean.ToMessageData Lean.Expr
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- The equivalence `x ↦ ωxω` as an operation on Lie submodules of the Geck construction.  -/
RootPairing.GeckConstruction.ωConjLieSubmodule : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} →
                    [inst_5 : P.IsCrystallographic] →
                      {b : P.Base} →
                        [inst_6 : Finite ι] →
                          [inst_7 : IsDomain R] →
                            [inst_8 : CharZero R] →
                              [inst_9 : DecidableEq ι] →
                                [inst_10 : Fintype ι] →
                                  LieSubmodule R (↥(RootPairing.GeckConstruction.lieAlgebra b)) (↥b.support ⊕ ι → R) →
                                    LieSubmodule R (↥(RootPairing.GeckConstruction.lieAlgebra b)) (↥b.support ⊕ ι → R)
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.instIsId : ∀ {M : Type u_4} [inst : Monoid M], MonoidHom.CompTriple.IsId (MonoidHom.id M)
-- Batteries.Util.Cache
/-- Function for adding a declaration from the library to the cache.
Defaults to the same behaviour as adding a declaration from the current file.  -/
Batteries.Tactic.DeclCache.addLibraryDecl : {α : Type} → Batteries.Tactic.DeclCache α → Lean.Name → Lean.ConstantInfo → α → Lean.MetaM α
-- Mathlib.Data.EReal.Operations
EReal.coe_mul_bot_of_pos : ∀ {x : ℝ}, 0 < x → ↑x * ⊥ = ⊥
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.sub : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s t : Set E},
  Balanced 𝕜 s → Balanced 𝕜 t → Balanced 𝕜 (s - t)
-- Mathlib.Topology.Homotopy.Contractible
ContractibleSpace.hequiv_unit' : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : ContractibleSpace X], Nonempty (ContinuousMap.HomotopyEquiv X Unit)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for signed less than `slt` on `BitVec`s.  -/
BitVec.reduceSLT : Lean.Meta.Simp.DSimproc
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsExtremal.congr_simp : ∀ {V : Type u_1} [inst : Fintype V] (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj] (p p_1 : SimpleGraph V → Prop),
      p = p_1 → G.IsExtremal p = G_1.IsExtremal p_1
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- Universe lift functor for finitely generated algebras.  -/
FGAlgCat.uliftFunctor : (R : Type u) → [inst : CommRing R] → CategoryTheory.Functor (FGAlgCat R) (FGAlgCat R)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.comp_h₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {G : CategoryTheory.PreOneHypercover S} (f : E.Hom F) (g : F.Hom G)
  {i j : E.I₀} (i_1 : E.I₁ i j), (f.comp g).h₁ i_1 = CategoryTheory.CategoryStruct.comp (f.h₁ i_1) (g.h₁ (f.s₁ i_1))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDerivWithin_sinh_Ioo : ∀ (n : ℕ) {a b x : ℝ}, x ∈ Set.Ioo a b → iteratedDerivWithin n Real.sinh (Set.Ioo a b) x = iteratedDeriv n Real.sinh x
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadInfoTree.getInfoState : {m : Type → Type} → [self : Lean.Elab.MonadInfoTree m] → m Lean.Elab.InfoState
-- Std.Do.Internal.Ensures.Lemmas
/-- `MonadAttach.CanReturn` implies `MayReturn` for `LawfulMonadAttach` instances.  -/
Std.Do.Internal.MayReturn.of_canReturn : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [LawfulMonadAttach m] {x : m α} {a : α}, MonadAttach.CanReturn x a → Std.Do.Internal.MayReturn x a
-- Mathlib.SetTheory.Ordinal.Notation
instDecidableEqONote.decEq : (x x_1 : ONote) → Decidable (x = x_1)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.instInhabited : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Inhabited (PolynomialModule R M)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap'_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂) h₂.i =
    CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instOption : {α : Type} → [Lean.Elab.ConfigEval.EvalTerm α] → Lean.Elab.ConfigEval.EvalTerm (Option α)
-- Init.Data.Range.Lemmas
Std.Legacy.Range.mem_of_mem_range' : ∀ {x : ℕ} {r : Std.Legacy.Range}, x ∈ List.range' r.start r.size r.step → x ∈ r
-- Mathlib.Topology.Order.OrderClosed
ContinuousWithinAt.closure_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : TopologicalSpace β] {f g : β → α} {s : Set β} {x : β},
  x ∈ closure s → ContinuousWithinAt f s x → ContinuousWithinAt g s x → (∀ y ∈ s, f y ≤ g y) → f x ≤ g x
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.NullMeasurable.comp_quasiMeasurePreserving : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → β} {g : β → γ},
  MeasureTheory.NullMeasurable g ν →
    MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → MeasureTheory.NullMeasurable (g ∘ f) μ
-- Lean.Meta.Tactic.Grind.Types
/-- A mapping `(a, b) ↦ is` s.t. for each `SplitInfo.arg a b i eq`
in `candidates` or `lookaheads` we have `i ∈ is`.
We use this information to decide whether the split/lookahead is "ready"
to be tried or not.
 -/
Lean.Meta.Grind.Split.State.argPosMap : Lean.Meta.Grind.Split.State → Std.HashMap (Lean.Expr × Lean.Expr) (List ℕ)
-- Lean.Declaration
Lean.instBEqConstantVal : BEq Lean.ConstantVal
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
ContinuousAlternatingMap.differentiable : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [Finite ι] (f : E [⋀^ι]→L[𝕜] F), Differentiable 𝕜 ⇑f
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.eq_of_not_ssuperset`.

---

**Alias** of `LE.le.eq_of_not_ssubset'`.

---

Set notation form of `LE.le.eq_of_not_lt'` -/
HasSubset.Subset.eq_of_not_ssuperset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, b ⊆ a → ¬b ⊂ a → a = b
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_eq_head?_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t.min? = t.toList.head?
-- Mathlib.FieldTheory.Separable
Algebra.IsSeparable.isSeparable : ∀ (F : Type u_1) {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K] [Algebra.IsSeparable F K]
  (x : K), IsSeparable F x
-- Std.Async.Signal
Std.Async.Signal.ofNat : ℕ → Std.Async.Signal
-- Mathlib.Algebra.Polynomial.FieldDivision
_private.Mathlib.Algebra.Polynomial.FieldDivision.0.Polynomial.quotient_mul_add_remainder_eq_aux : ∀ {R : Type u} [inst : Field R] (p q : Polynomial R), q * p.div q + p.mod q = p
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link2.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (r r' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.Tree α β (r'.size + r.size) → Sort u_3) (ℓ : Std.DTreeMap.Internal.Impl α β)
  (hℓ₁ : ℓ.Balanced) (hℓ₂ : ℓ.size = r'.size + r.size)
  (h_1 :
    (ℓ : Std.DTreeMap.Internal.Impl α β) →
      (hℓ₁ : ℓ.Balanced) →
        (hℓ₂ : ℓ.size = r'.size + r.size) → motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }),
  (match { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } with
    | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } => h_1 ℓ hℓ₁ hℓ₂) =
    h_1 ℓ hℓ₁ hℓ₂
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.lt_iff_exists_eq_append : ∀ {s : String} {p₁ p₂ : s.Pos} {t₁ t₂ t₃ t₄ : String},
  p₁.Splits t₁ t₂ → p₂.Splits t₃ t₄ → (p₁ < p₂ ↔ ∃ t₅, t₅ ≠ "" ∧ t₃ = t₁ ++ t₅ ∧ t₂ = t₅ ++ t₄)
-- Std.Http.Internal.IndexMultiMap
Std.Internal.IndexMultiMap.instUnionOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → [EquivBEq α] → [LawfulHashable α] → Union (Std.Internal.IndexMultiMap α β)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- The inner product of a vector with a multiple of itself.  -/
real_inner_smul_self_right : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x : F) (r : ℝ),
  inner ℝ x (r • x) = r * (‖x‖ * ‖x‖)
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.ofHom_hom : ∀ {R : Type u} [inst : CommRing R] {S T : Type v} [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] [inst_5 : Module.Finite R S] [inst_6 : Algebra.Etale R S] [inst_7 : Module.Finite R T]
  [inst_8 : Algebra.Etale R T] (f : S →ₐ[R] T), (CommAlgCat.FiniteEtale.ofHom f).hom = CommAlgCat.ofHom f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_some_get!_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α},
  m.contains a = true → Std.ExtDHashMap.Const.get? m a = some (Std.ExtDHashMap.Const.get! m a)
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_neg : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N] (f g : α →₀ N),
  (-f).neLocus g = f.neLocus (-g)
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filterGen<_» : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.card_add_card_subsetSum_lt_card_subsetSum_insert_max : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A : Finset M} {a : M} [inst_2 : LinearOrder M]
  [IsOrderedCancelAddMonoid M],
  (∀ x ∈ A, 0 < x) → (∀ x ∈ A, x < a) → 0 < a → A.card + A.subsetSum.card < (insert a A).subsetSum.card
-- Lean.MonadEnv
Lean.hasConst : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → optParam Bool true → m Bool
-- Lean.Parser.Term
Lean.Parser.Term.binrel.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.SInt.Lemmas
Int16.mod_one : ∀ {a : Int16}, a % 1 = 0