mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The carrier of an additive subsemigroup.  -/
AddSubsemigroup.carrier : {M : Type u_3} → [inst : Add M] → AddSubsemigroup M → Set M
-- Lean.Server.InfoUtils
Lean.Elab.InfoTree.foldInfo : {α : Type u_1} → (Lean.Elab.ContextInfo → Lean.Elab.Info → α → α) → α → Lean.Elab.InfoTree → α
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.compress.go : String → Lean.Json.CompressWorkItemQueue✝ → String
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousAt_iSup : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {f : ι → α → δ}, (∀ (i : ι), LowerSemicontinuousAt (f i) x) → LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.keys.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List ((a : α) × β a) → Sort u_3) (k : α) (snd : β k)
  (l : List ((a : α) × β a)) (h_1 : Unit → motive [])
  (h_2 : (k : α) → (snd : β k) → (l : List ((a : α) × β a)) → motive (⟨k, snd⟩ :: l)),
  (match ⟨k, snd⟩ :: l with
    | [] => h_1 ()
    | ⟨k, snd⟩ :: l => h_2 k snd l) =
    h_2 k snd l
-- Mathlib.Combinatorics.Matroid.Closure
/-- This can be used for rewriting if the LHS is inside a binder and it is unknown
whether `f = e`.  -/
Matroid.Indep.insert_sdiff_indep_iff : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α},
  M.Indep (I \ {e}) → e ∈ I → (M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
AdjoinRoot.powerBasis'.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic),
  AdjoinRoot.powerBasis' hg = AdjoinRoot.powerBasis' hg
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- A hom equivalence over the function `OneTruncation₂.nerveEquiv`.  -/
SSet.OneTruncation₂.nerveHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : SSet.OneTruncation₂ ((SSet.truncation 2).obj (CategoryTheory.nerve C))} →
      (X ⟶ Y) ≃ (SSet.OneTruncation₂.nerveEquiv X ⟶ SSet.OneTruncation₂.nerveEquiv Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- **Alias** of `CategoryTheory.Limits.productUniqueIso_inv_π`. -/
CategoryTheory.Limits.productUniqueIso_inv : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : Unique β] (f : β → C) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.productUniqueIso f).inv (CategoryTheory.Limits.Pi.π f b) =
    CategoryTheory.eqToHom ⋯
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.mk : {H : Type u_5} →
  [inst : TopologicalSpace H] →
    {M : Type u_6} →
      [inst_1 : TopologicalSpace M] →
        (atlas : Set (OpenPartialHomeomorph M H)) →
          (chartAt : M → OpenPartialHomeomorph M H) →
            (∀ (x : M), x ∈ (chartAt x).source) → (∀ (x : M), chartAt x ∈ atlas) → ChartedSpace H M
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.sub_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s t : Set G},
  IsOpen s → IsOpen (s - t)
-- Mathlib.Order.SuccPred.Basic
instSuccOrderOrderDualOfPredOrder : {α : Type u_1} → [inst : Preorder α] → [PredOrder α] → SuccOrder αᵒᵈ
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocSemiring.toAddCommMonoid : {α : Type u} → [self : NonUnitalNonAssocSemiring α] → AddCommMonoid α
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_apply : ∀ {n : ℕ} (i : Fin n), (finRotate n) i = i + 1
-- Init.Data.String.Basic
String.Slice.Pos.offset_next : ∀ {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos}, (pos.next h).offset = pos.offset + pos.get h
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Alternative constructor for `isWeakLimit`,
providing a morphism of cones rather than a morphism between the cone points
and separately the factorisation condition.
 -/
CategoryTheory.Limits.IsWeakLimit.mkOfConeMorphism : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            ((s : CategoryTheory.Limits.Cone F) → s ⟶ t) → CategoryTheory.Limits.IsWeakLimit t
-- Mathlib.Algebra.Ring.Units
isUnit_neg_one : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α], IsUnit (-1)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- action on objects  -/
CategoryTheory.StrictlyUnitaryLaxFunctorCore.obj : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.StrictlyUnitaryLaxFunctorCore B C → B → C
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_trans_self : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.trans e = Equiv.refl β
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.ext' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (f g : T₁ ⟶ T₂),
  f.app = g.app → f = g
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_finset_univ : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α] [inst_3 : Fintype α],
  MulAction.stabilizer G Finset.univ = ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  t.alter k f ≠ ∅ →
    ∀ {fallback : α},
      (t.alter k f).minKeyD fallback = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Init.Data.UInt.Lemmas
USize.toUInt64_toUInt16 : ∀ (n : USize), n.toUInt16.toUInt64 = n.toUInt64 % 65536
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flip_f₂₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.flip.f₂₄ = sq.f₃₄
-- Mathlib.Topology.Coherent
/-- If `X` is a sequential space
and `S` contains each set of the form `insert x (Set.range u)`
where `u : ℕ → X` is a sequence and `x` is its limit,
then topology on `X` is generated by its restrictions to the sets of `S`.  -/
Topology.IsCoherentWith.of_seq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)} [SequentialSpace X],
  (∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Filter.Tendsto u Filter.atTop (nhds x) → insert x (Set.range u) ∈ S) →
    Topology.IsCoherentWith S
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley.eq_1 : ∀ {M : Type u_1} (s : Set M) [inst : Add M],
  SimpleGraph.addCayley s = SimpleGraph.fromRel fun x1 x2 => ∃ g ∈ s, x1 + g = x2
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : α → E}
  {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0),
  MeasureTheory.Integrable f μ → ((μ.withDensityᵥ f).trim hm).AbsolutelyContinuous (μ.trim hm).toENNRealVectorMeasure
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol_injective : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [Nonempty ι], Function.Injective (Matrix.replicateCol ι)
-- Mathlib.Topology.UniformSpace.Equicontinuity
Filter.HasBasis.equicontinuousAt_iff_right : ∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α]
  {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {x₀ : X},
  (uniformity α).HasBasis p s →
    (EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k)
-- Init.Data.Option.Basic
Option.min_some_some : ∀ {α : Type u_1} [inst : Min α] {a b : α}, some a ⊓ some b = some (a ⊓ b)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.iterM_toArray : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n}, xs.toArray.iterM m = xs.iterM m
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.internalIter_eq.match_1.eq_1 : ∀ (motive : Option ℕ → Sort u_1) (stop : ℕ) (h_1 : (stop : ℕ) → motive (some stop)) (h_2 : Unit → motive none),
  (match some stop with
    | some stop => h_1 stop
    | none => h_2 ()) =
    h_1 stop
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_ofHom : ∀ {k : Type u} {G : Type v} {X Y : Type w} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G]
  [inst_3 : AddCommGroup X] [inst_4 : Module k X] [inst_5 : TopologicalSpace X] [inst_6 : IsTopologicalAddGroup X]
  [inst_7 : ContinuousSMul k X] [inst_8 : AddCommGroup Y] [inst_9 : Module k Y] [inst_10 : TopologicalSpace Y]
  [inst_11 : IsTopologicalAddGroup Y] [inst_12 : ContinuousSMul k Y] {ρ : ContRepresentation k G X}
  {σ : ContRepresentation k G Y} (f : ContIntertwiningMap ρ σ), TopRep.Hom.hom (TopRep.ofHom f) = f
-- Mathlib.RingTheory.Etale.StandardEtale
/-- An `AlgEquiv` between `P.Ring` and `R[X][Y]/⟨f, Yg-1⟩`,
to not abuse the defeq between the two.  -/
StandardEtalePair.equivPolynomialQuotient : {R : Type u_1} →
  [inst : CommRing R] →
    (P : StandardEtalePair R) →
      P.Ring ≃ₐ[R] Polynomial (Polynomial R) ⧸ Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1}
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.hom_comp : ∀ {M N T : AddMagmaCat} (f : M ⟶ N) (g : N ⟶ T),
  AddMagmaCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (AddMagmaCat.Hom.hom g).comp (AddMagmaCat.Hom.hom f)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetMapIsOpenImmersion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.map f)
-- Mathlib.Data.NNReal.Defs
NNReal.coe_nonneg : ∀ (r : NNReal), 0 ≤ ↑r
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_map : ∀ {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : Std.Internal.Do.Assertion Pred]
  [inst_4 : Std.Internal.Do.Assertion EPred] [inst_5 : Std.Internal.Do.WPMonad n Pred EPred] [inst_6 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [inst_8 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_10 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P : Pred}
  {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄ forIn it init fun out acc => g (f out) acc ⦃ Q; eQ ⦄ → ⦃ P ⦄ forIn (Std.IterM.map f it) init g ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_nonneg_iff : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R] [NeZero 1]
  {n : ℤ}, 0 ≤ ↑n ↔ 0 ≤ n
-- Mathlib.Data.Num.Basic
instInhabitedNum : Inhabited Num
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.Limits.HasZeroObject C} {inst_3 : CategoryTheory.HasShift C ℤ}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst_5 : CategoryTheory.Pretriangulated C}
  {le ge : ℤ → CategoryTheory.ObjectProperty C}
  {le_isClosedUnderIsomorphisms :
    autoParam (∀ (n : ℤ), (le n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam}
  {ge_isClosedUnderIsomorphisms :
    autoParam (∀ (n : ℤ), (ge n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam}
  {le_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le n X → le n' ((CategoryTheory.shiftFunctor C a).obj X)}
  {ge_shift : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), ge n X → ge n' ((CategoryTheory.shiftFunctor C a).obj X)}
  {zero' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), le 0 X → ge 1 Y → f = 0} {le_zero_le : le 0 ≤ le 1} {ge_one_le : ge 1 ≤ ge 0}
  {exists_triangle_zero_one :
    ∀ (A : C),
      ∃ X Y,
        ∃ (_ : le 0 X) (_ : ge 1 Y),
          ∃ f g h,
            CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {le_1 ge_1 : ℤ → CategoryTheory.ObjectProperty C}
  {le_isClosedUnderIsomorphisms_1 :
    autoParam (∀ (n : ℤ), (le_1 n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.le_isClosedUnderIsomorphisms._autoParam}
  {ge_isClosedUnderIsomorphisms_1 :
    autoParam (∀ (n : ℤ), (ge_1 n).IsClosedUnderIsomorphisms)
      CategoryTheory.Triangulated.TStructure.ge_isClosedUnderIsomorphisms._autoParam}
  {le_shift_1 : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), le_1 n X → le_1 n' ((CategoryTheory.shiftFunctor C a).obj X)}
  {ge_shift_1 : ∀ (n a n' : ℤ), a + n' = n → ∀ (X : C), ge_1 n X → ge_1 n' ((CategoryTheory.shiftFunctor C a).obj X)}
  {zero'_1 : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), le_1 0 X → ge_1 1 Y → f = 0} {le_zero_le_1 : le_1 0 ≤ le_1 1}
  {ge_one_le_1 : ge_1 1 ≤ ge_1 0}
  {exists_triangle_zero_one_1 :
    ∀ (A : C),
      ∃ X Y,
        ∃ (_ : le_1 0 X) (_ : ge_1 1 Y),
          ∃ f g h,
            CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles},
  { le := le, ge := ge, le_isClosedUnderIsomorphisms := le_isClosedUnderIsomorphisms,
        ge_isClosedUnderIsomorphisms := ge_isClosedUnderIsomorphisms, le_shift := le_shift, ge_shift := ge_shift,
        zero' := zero', le_zero_le := le_zero_le, ge_one_le := ge_one_le,
        exists_triangle_zero_one := exists_triangle_zero_one } =
      { le := le_1, ge := ge_1, le_isClosedUnderIsomorphisms := le_isClosedUnderIsomorphisms_1,
        ge_isClosedUnderIsomorphisms := ge_isClosedUnderIsomorphisms_1, le_shift := le_shift_1, ge_shift := ge_shift_1,
        zero' := zero'_1, le_zero_le := le_zero_le_1, ge_one_le := ge_one_le_1,
        exists_triangle_zero_one := exists_triangle_zero_one_1 } →
    le = le_1 ∧ ge = ge_1
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_inv_Iio : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : PartialOrder G] [inst_3 : CommGroup G] [IsOrderedMonoid G] [MeasurableInv G] [μ.IsInvInvariant] {c : G}
  {f : G → F}, MeasureTheory.IntegrableOn f (Set.Ioi c⁻¹) μ → MeasureTheory.IntegrableOn (fun x => f x⁻¹) (Set.Iio c) μ
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_zero : ∀ (X : Type u_1) {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] [inst_2 : Zero Y]
  (r : NNReal), eHolderNorm r 0 = 0
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_support : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData},
  AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal I.support = I.radical
-- Mathlib.Topology.VectorBundle.Basic
/-- One of the standard local trivializations of a vector bundle constructed from core, taken by
considering this in particular as a fiber bundle constructed from core.  -/
VectorBundleCore.localTriv : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} → (Z : VectorBundleCore R B F ι) → ι → Bundle.Trivialization F Bundle.TotalSpace.proj
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The Weierstrass curve in Jacobian coordinates base changed to an algebra `S` over `R`.  -/
WeierstrassCurve.Jacobian.baseChange : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Jacobian R → (S : Type s) → [inst_1 : CommRing S] → [Algebra R S] → WeierstrassCurve.Jacobian S
-- Mathlib.Logic.Equiv.Multiset
/-- Outputs the list of partial sums of the input list, that is
`raise [a₁, a₂, ...] n = [n + a₁, n + a₁ + a₂, ...]`  -/
Denumerable.raise : List ℕ → ℕ → List ℕ
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.IsPathGraph3Compl.not_adj_snd : ∀ {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α}, G.IsPathGraph3Compl v w₁ w₂ → ¬G.Adj v w₂
-- Lean.Parser.Command
Lean.Parser.Command.structSimpleBinder : Lean.Parser.Parser
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxcHasSize.eq_1 : Int32.instRxcHasSize = { size := fun lo hi => (hi.toInt + 1 - lo.toInt).toNat }
-- Lean.Environment
Lean.instInhabitedEffectiveImport : Inhabited Lean.EffectiveImport
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertMany_ind : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)]
  {motive : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Prop} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α) (b : β), motive m → motive (m.insert a b)) →
      motive ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_eq_empty_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → Set.Ioo a b = ∅
-- Mathlib.Analysis.SpecialFunctions.Sqrt
derivWithin_sqrt : ∀ {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ},
  DifferentiableWithinAt ℝ f s x →
    f x ≠ 0 → UniqueDiffWithinAt ℝ s x → derivWithin (fun x => √(f x)) s x = derivWithin f s x / (2 * √(f x))
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.iSup_filtration_iio : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) [OrderBot ι]
  [SuccOrder ι] (m : ι), Order.IsSuccLimit m → ⨆ i, f.filtration ↑i = f.filtration m
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.containsThenInsert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α}
  {b : β a}, t.WF → (t.containsThenInsert a b).2.WF
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `AddGroup` across an `Equiv`  -/
Equiv.addGroup : {α : Type u_2} → {β : Type u_3} → α ≃ β → [AddGroup β] → AddGroup α
-- Mathlib.Algebra.Order.Ring.Abs
dvd_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] (a b : α), a ∣ |b| ↔ a ∣ b
-- Batteries.Data.BitVec.Lemmas
BitVec.toInt_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool), (BitVec.ofFnLE f).toInt = Int.ofBits f
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The `leftInv` direction of the equivalence  -/
YoungDiagram.ofRowLens_to_rowLens_eq_self : ∀ {μ : YoungDiagram}, YoungDiagram.ofRowLens μ.rowLens ⋯ = μ
-- Std.Http.Data.Body.Stream
/-- Creates a rendezvous body stream.
 -/
Std.Http.Body.mkStream : Std.Async.Async Std.Http.Body.Stream
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.monomialOneHom_apply : ∀ {R : Type u} {σ : Type u_1} {s : σ →₀ ℕ} [inst : CommSemiring R],
  (MvPolynomial.monomialOneHom R σ) s = (MvPolynomial.monomial s) 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for strict reverse monotonicity of addition on the left,
namely `a + b₁ < a + b₂ → b₁ < b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedAddMonoid`.  -/
AddLeftReflectLT : (M : Type u_1) → [Add M] → [LT M] → Prop
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.esymm_summand_to_weight : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : Fintype σ] (k : ℕ),
  ∀ A ∈ Finset.powersetCard k Finset.univ,
    ∑ j ∈ A, MvPolynomial.NewtonIdentities.weight✝ σ R k (A, j) = ↑k * (-1) ^ k * ∏ i ∈ A, MvPolynomial.X i
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSMul'.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α], Lex.instSMul' = inst
-- Mathlib.Analysis.Calculus.Gradient.Basic
HasGradientAtFilter.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {L : Filter F} {f₁ : F → 𝕜},
  HasGradientAtFilter f f' x L → f₁ =ᶠ[L] f → f₁ x = f x → HasGradientAtFilter f₁ f' x L
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso_inv_app_app_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (X_1 : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_2 : X),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).unitIso.inv.app X_1).app X_2).fst =
    CategoryTheory.CategoryStruct.id (X_1.obj X_2).fst
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.maxEntry?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.maxEntry? = t₂.maxEntry?
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_of_injOn_mapsTo : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β},
  Set.InjOn f s → Set.MapsTo f s t → s.Infinite → t.Infinite
-- Init.Data.String.Substring
Substring.isEmpty : Substring.Raw → Bool
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.LetRecClosure.mk : Lean.Syntax →
  Array Lean.LocalDecl → Lean.Expr → Lean.Elab.Term.LetRecToLift → Lean.Elab.Term.MutualClosure.LetRecClosure
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivWithinAt.neg` -/
HasFDerivWithinAt.fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E}, HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun i => -f i) (-f') s x
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instLawfulUpwardEnumerable : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerable (BitVec n)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- When running the "tryAtEachStep" tactic analysis linters,
only run on a fraction `1/n` of the goals found in the library.

This is useful for running quick benchmarks.
 -/
linter.tacticAnalysis.tryAtEachStep.fraction : Lean.Option ℕ
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_lt_rpow : ∀ {x y : ENNReal} {z : ℝ}, x < y → 0 < z → x ^ z < y ^ z
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- The `n`th elementary symmetric function evaluated at the elements of `s`  -/
Multiset.esymm : {R : Type u_1} → [CommSemiring R] → Multiset R → ℕ → R
-- Mathlib.Order.Nucleus
Nucleus.iInf_apply : ∀ {X : Type u_1} [inst : CompleteLattice X] {ι : Type u_2} (f : ι → Nucleus X) (x : X), (iInf f) x = ⨅ j, (f j) x
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instMulMemClass : ∀ {M : Type u_1} [inst : Mul M], MulMemClass (Subsemigroup M) M
-- Mathlib.Order.Monotone.MonovaryOrder
MonovaryOrder.eq_1 : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] (f : ι → α) (g : ι → β)
  (i j : ι),
  MonovaryOrder f g i j =
    Prod.Lex (fun x1 x2 => x1 < x2) (Prod.Lex (fun x1 x2 => x1 < x2) WellOrderingRel) (f i, g i, i) (f j, g j, j)
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.comp_snd : ∀ {X Y Z : TopPair} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : TopPair.Homotopy g₀ g₁) (F : TopPair.Homotopy f₀ f₁),
  (G.comp F).snd = G.snd.comp F.snd