mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, panicking if no such element exists.
 -/
Std.TreeSet.getLE! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet α cmp → α → α
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance.eq_1 : ∀ (pat : String.Slice) (patByte : UInt8) (table : Array ℕ) (ht : table.size ≤ pat.utf8ByteSize)
  (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) (guess : ℕ) (hg : guess < table.size),
  String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h guess hg =
    if pat.getUTF8Byte { byteIdx := guess } ⋯ = patByte then ⟨guess + 1, ⋯⟩
    else
      if h₀ : guess = 0 then ⟨0, ⋯⟩
      else
        have this := ⋯;
        String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h table[guess - 1] ⋯
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
/-- Extension for the `positivity` tactic: `SzemerediRegularity.initialBound` is always positive.  -/
Mathlib.Meta.Positivity.evalInitialBound : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the reverse direction of `Asymptotics.isTheta_norm_right`. -/
Asymptotics.IsTheta.norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =Θ[l] g' → f =Θ[l] fun x => ‖g' x‖
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Sigma.ι_π_eq_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasCoproduct f] (b : β) {Z : C}
  (h : f b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.π f b) h) =
    h
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ColorInformation.mk.sizeOf_spec : ∀ (range : Lean.Lsp.Range) (color : Lean.Lsp.Color),
  sizeOf { range := range, color := color } = 1 + sizeOf range + sizeOf color
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_eq_minD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t.min! = t.minD default
-- Std.Tactic.Do.ProofMode
Std.Tactic.Do.mgoalHyp : Lean.ParserDescr
-- Mathlib.Algebra.Order.Archimedean.Basic
le_of_forall_rat_lt_imp_le : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K},
  (∀ (q : ℚ), ↑q < x → ↑q ≤ y) → x ≤ y
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Tensor product over a singleton type with element `i₀` is equivalent to `s i₀`.  -/
PiTensorProduct.subsingletonEquiv : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            [Subsingleton ι] → (i₀ : ι) → (PiTensorProduct R fun i => s i) ≃ₗ[R] s i₀
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.eq_cuspFunction : ∀ {h : ℝ} {f : ℂ → ℂ},
  h ≠ 0 → Function.Periodic f ↑h → ∀ (z : ℂ), Function.Periodic.cuspFunction h f (Function.Periodic.qParam h z) = f z
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.ext'_iff : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} {f g : X ⟶ Y}, f = g ↔ f.toHom = g.toHom
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural embedding `N →* M ∗ N`.  -/
Monoid.Coprod.inr : {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → N →* Monoid.Coprod M N
-- Mathlib.Data.String.Defs
/-- Produce the head character from the string `s`, if `s` is not empty, otherwise `'A'`.  -/
String.head : String → Char
-- Mathlib.Data.Set.Lattice.Image
Set.prod_image_seq_comm : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), (Prod.mk '' s).seq t = ((fun b a => (a, b)) '' t).seq s
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.hasFDerivAt_fourierChar_neg_bilinear_left : ∀ {V : Type u_1} {W : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : NormedAddCommGroup W]
  [inst_3 : NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (v : V) (w : W),
  HasFDerivAt (fun v => ↑(Real.fourierChar (-(L v) w)))
    ((-2 * ↑Real.pi * Complex.I * ↑(Real.fourierChar (-(L v) w))) • Complex.ofRealCLM ∘SL L.flip w) v
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.mkSol.eq_def : ∀ {R : Type u_1} [inst : CommSemiring R] (E : LinearRecurrence R) (init : Fin E.order → R) (x : ℕ),
  E.mkSol init x =
    let n := x;
    if h : n < E.order then init ⟨n, h⟩
    else
      ∑ k,
        have x := ⋯;
        E.coeffs k * E.mkSol init (n - E.order + ↑k)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticTag : Inhabited Lean.Lsp.DiagnosticTag
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiff.inv₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] {E' : Type u_5}
  [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_10 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M]
  {f : M → G} [ContMDiffInv₀ I n G], ContMDiff I' I n f → (∀ (x : M), f x ≠ 0) → ContMDiff I' I n fun x => (f x)⁻¹
-- Init.Data.Int.Basic
instIntCastInt : IntCast ℤ
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixedPoints_addSubgroup_sup : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {P Q : AddSubgroup M},
  AddAction.fixedPoints (↥(P ⊔ Q)) α = AddAction.fixedPoints (↥P) α ∩ AddAction.fixedPoints (↥Q) α
-- Mathlib.Order.Category.DistLat
/-- The category of distributive lattices.  -/
DistLat : Type (u_1 + 1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey_modifyKey_eq_minKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [Std.LawfulEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {he : (Std.Internal.List.Const.modifyKey k f l).isEmpty = false},
      Std.Internal.List.minKey (Std.Internal.List.Const.modifyKey k f l) he = Std.Internal.List.minKey l ⋯
-- Mathlib.Order.Hom.Basic
OrderIso.coe_dualDual_symm : ∀ (α : Type u_2) [inst : LE α], ⇑(OrderIso.dualDual α).symm = ⇑OrderDual.ofDual ∘ ⇑OrderDual.ofDual
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.isubtree.eq_2 : ∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (x : F.M) (a : F.A) (i : F.B a)
  (ps : List F.Idx),
  PFunctor.M.isubtree (⟨a, i⟩ :: ps) x =
    x.casesOn' fun a' f => if h : a = a' then PFunctor.M.isubtree ps (f (cast ⋯ i)) else default
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.instInv : {M : Type u_1} → Inv (Mathlib.Tactic.FieldSimp.NF M)
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology : ∀ {X : AlgebraicGeometry.Scheme} {s : CategoryTheory.Sieve X},
  s ∈ AlgebraicGeometry.Scheme.jointlySurjectiveTopology X ↔
    s.arrows ∈ AlgebraicGeometry.Scheme.jointlySurjectivePretopology.coverings X
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn_pure_yield_eq_fold : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {f : β → γ → γ} {init : γ} {it : Std.Iter β},
  (forIn it init fun c b => pure (ForInStep.yield (f c b))) = pure (Std.Iter.fold (fun b c => f c b) init it)
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.equivFinsupp_symm_apply : ∀ (X : Type u_1) (a : X →₀ ℤ), (FreeAbelianGroup.equivFinsupp X).symm a = Finsupp.toFreeAbelianGroup a
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.SymbolPriorityEntry.mk.inj : ∀ {declName : Lean.Name} {prio : ℕ} {declName_1 : Lean.Name} {prio_1 : ℕ},
  { declName := declName, prio := prio } = { declName := declName_1, prio := prio_1 } →
    declName = declName_1 ∧ prio = prio_1
-- Mathlib.Geometry.Manifold.SmoothEmbedding
_private.Mathlib.Geometry.Manifold.SmoothEmbedding.0.Manifold.IsSmoothEmbedding.comp : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E₁ : Type u_2} →
      {E₃ : Type u_4} →
        {E₄ : Type u_5} →
          [inst_1 : NormedAddCommGroup E₁] →
            [inst_2 : NormedSpace 𝕜 E₁] →
              [inst_3 : NormedAddCommGroup E₃] →
                [inst_4 : NormedSpace 𝕜 E₃] →
                  [inst_5 : NormedAddCommGroup E₄] →
                    [inst_6 : NormedSpace 𝕜 E₄] →
                      {H : Type u_6} →
                        {G : Type u_8} →
                          {G' : Type u_9} →
                            [inst_7 : TopologicalSpace H] →
                              [inst_8 : TopologicalSpace G] →
                                [inst_9 : TopologicalSpace G'] →
                                  {I : ModelWithCorners 𝕜 E₁ H} →
                                    {J : ModelWithCorners 𝕜 E₃ G} →
                                      {J' : ModelWithCorners 𝕜 E₄ G'} →
                                        {M : Type u_10} →
                                          {N : Type u_12} →
                                            {N' : Type u_13} →
                                              [inst_10 : TopologicalSpace M] →
                                                [inst_11 : ChartedSpace H M] →
                                                  [inst_12 : TopologicalSpace N] →
                                                    [inst_13 : ChartedSpace G N] →
                                                      [inst_14 : TopologicalSpace N'] →
                                                        [inst_15 : ChartedSpace G' N'] →
                                                          {n : WithTop ℕ∞} →
                                                            {f : M → N} →
                                                              {g : N → N'} →
                                                                Manifold.IsSmoothEmbedding J J' n g →
                                                                  Manifold.IsSmoothEmbedding I J n f →
                                                                    ProofWanted
                                                                      (Manifold.IsSmoothEmbedding I J' n (g ∘ f))
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.cocycle₁'.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct),
  CochainComplex.Lifting.cocycle₁' sq hsq =
    CochainComplex.HomComplex.Cocycle.mk (CochainComplex.HomComplex.δ 0 1 (CochainComplex.Lifting.cochain₀ sq hsq)) 2
      CochainComplex.Lifting.cocycle₁'._proof_1 ⋯
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- The map `(p, q) ↦ f * q + g * p` whose associated matrix is `Syl(f, g)`.  -/
Polynomial.sylvesterMap : {m n : ℕ} →
  {R : Type u_1} →
    [inst : CommRing R] →
      (f g : Polynomial R) →
        f.natDegree ≤ m →
          g.natDegree ≤ n →
            ↥(Polynomial.degreeLT R m) × ↥(Polynomial.degreeLT R n) →ₗ[R] ↥(Polynomial.degreeLT R (m + n))
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.instMulActionSubtypeAEEqFunMemAddSubgroupLp : {M : Type u_1} →
  {α : Type u_3} →
    {E : Type u_4} →
      [inst : MeasurableSpace α] →
        [inst_1 : NormedAddCommGroup E] →
          {μ : MeasureTheory.Measure α} →
            {p : ENNReal} →
              [inst_2 : Monoid M] →
                [inst_3 : MulAction M α] →
                  [MeasureTheory.SMulInvariantMeasure M α μ] →
                    [MeasurableConstSMul M α] → MulAction Mᵈᵐᵃ ↥(MeasureTheory.Lp E p μ)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry?ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α β) (k : α),
  l.getEntry?ₘ k = Std.DTreeMap.Internal.Impl.applyCell k l fun c x => c.getEntry?
-- Batteries.Data.UInt
UInt32.max_def : ∀ (x y : UInt32), x ⊔ y = if x ≤ y then y else x
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.star_add_self : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : StarAddMonoid R] (x : R), IsSelfAdjoint (star x + x)
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If a functor creates equalizers and the appropriate products, it creates limits.

We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating limits" in the literature, and whether or not the condition can be dropped seems to depend
on the specific definition that is used.  -/
CategoryTheory.Limits.createsLimitsOfShapeOfCreatesEqualizersAndProducts : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        {D : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
            [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) D] →
              [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) D] →
                [CategoryTheory.Limits.HasEqualizers D] →
                  (G : CategoryTheory.Functor C D) →
                    [G.ReflectsIsomorphisms] →
                      [CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] →
                        [CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) G] →
                          [CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2)))
                                G] →
                            CategoryTheory.CreatesLimitsOfShape J G
-- Mathlib.Order.Bounds.OrderIso
OrderIso.isLUB_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {s : Set β} {x : α},
  IsLUB (⇑f ⁻¹' s) x ↔ IsLUB s (f x)
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ne_of_ne : ∀ {a b : UInt64}, a ≠ b → a.toBitVec ≠ b.toBitVec
-- Mathlib.Algebra.Group.Action.Defs
/-- Associativity of `•`  -/
IsScalarTower.smul_assoc : ∀ {M : Type u_9} {N : Type u_10} {α : Type u_11} {inst : SMul M N} {inst_1 : SMul N α} {inst_2 : SMul M α}
  [self : IsScalarTower M N α] (x : M) (y : N) (z : α), (x • y) • z = x • y • z
-- Mathlib.Algebra.Group.AddChar
AddChar.sub_apply : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : CommMonoid M] (ψ χ : AddChar A M) (a : A),
  (ψ - χ) a = ψ a * χ (-a)
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.finBicone : (J : Type u₁) → [Fintype J] → Fintype (CategoryTheory.Bicone J)
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.save : Lean.Expr → Lean.MetaM ProofWidgets.ExprWithCtx
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.exists_or_of_range_m_N : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (s : (SSet.Subcomplex.range (f.m j)).N),
  ∃ c, s = SSet.Subcomplex.Pairing.RankFunction.Cell.type₁ f c ∨ s = SSet.Subcomplex.Pairing.RankFunction.Cell.type₂ f c
-- Mathlib.Algebra.Order.GroupWithZero.Basic
div_nonpos_of_nonpos_of_nonneg : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [MulPosReflectLT G₀] {a b : G₀},
  a ≤ 0 → 0 ≤ b → a / b ≤ 0
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardCongr_hom_app_val_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] {φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R} (e : φ = ψ)
  (M : SheafOfModules R) (U : Cᵒᵖ) (x : ↑(((SheafOfModules.pushforward φ).obj M).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom (((SheafOfModules.pushforwardCongr e).hom.app M).val.app U)) x = x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (n m : ℤ) {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} D]
  [inst_3 : CategoryTheory.Preadditive D] (z : CochainComplex.HomComplex.Cochain K L n) (Φ : CategoryTheory.Functor C D)
  [inst_4 : Φ.Additive], CochainComplex.HomComplex.δ n m (z.map Φ) = (CochainComplex.HomComplex.δ n m z).map Φ
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence_inverse_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  (ι : Type u_1) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S)
  (A : (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra) (x x_1 : ι),
  ((CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence F ι f).inverse.obj A).hom x x_1 = A.a
-- Mathlib.Order.Lattice
inf_inf_distrib_right : ∀ {α : Type u} [inst : SemilatticeInf α] (a b c : α), a ⊓ b ⊓ c = a ⊓ c ⊓ (b ⊓ c)
-- Mathlib.Topology.Defs.Basic
/-- Delaborator for `IsOpen[_]`.  -/
Topology.delabIsOpen : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntry?.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) =
    h_2 size k v l
-- Init.Data.String.Substring
/-- Removes the longest prefix of a substring in which a Boolean predicate returns `true` for all
characters by moving the substring's start position. The start position is moved to the position of
the first character for which the predicate returns `false`, or to the substring's end position if
the predicate always returns `true`.
 -/
Substring.Raw.dropWhile : Substring.Raw → (Char → Bool) → Substring.Raw
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.instIsLocallySurjectiveFunToImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ G),
  CategoryTheory.Sheaf.IsLocallySurjective (CategoryTheory.Sheaf.toImage f)
-- Init.Data.Bool
/-- This should not be turned on globally as an instance because it degrades performance in Mathlib,
but may be used locally.
 -/
boolPredToPred : {α : Sort u_1} → Coe (α → Bool) (α → Prop)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- Supporting function for the `R[x₁,x₂,...,xₙ]` adjunction notation.  -/
Algebra.delabAdjoinNotation : Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcConnectParams : Lean.ToJson Lean.Lsp.RpcConnectParams
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffsIn_pow : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {n : ℕ}, n ≠ 0 → ∀ (M : Submodule R S), MvPolynomial.coeffsIn σ (M ^ n) = MvPolynomial.coeffsIn σ M ^ n
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.ae_eq_univ_iff_measure_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.NullMeasurableSet s μ → (s =ᵐ[μ] Set.univ ↔ μ s = μ Set.univ)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restrOpen_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s), (e.restrOpen s hs).source = e.source ∩ s
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ_σ₀Iter_assoc : ∀ {n : ℕ} (i : Fin (n + 2)) (j : ℕ) {m : ℕ} (h : autoParam (m + (j + 1) = n + 1) SimplexCategory.δ_σ₀Iter._auto_1),
  autoParam (↑i ≤ j + 1) SimplexCategory.δ_σ₀Iter._auto_3 →
    ∀ {Z : SimplexCategory} (h_1 : { len := m } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter (j + 1) h) h_1) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter j ⋯) h_1