mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.natCoe_nat : ∀ (f : ArithmeticFunction ℕ), ↑f = f
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
/-- `π C (· ∈ s)` is finite for a finite set `s`.  -/
Profinite.NobelingProof.instFintypeElemForallBoolπMemFinset : {I : Type u} →
  (C : Set (I → Bool)) → [inst : LinearOrder I] → (s : Finset I) → Fintype ↑(Profinite.NobelingProof.π C fun x => x ∈ s)
-- Std.Data.ExtTreeMap.Basic
/-- Transforms an array of keys into a tree map.  -/
Std.ExtTreeMap.unitOfArray : {α : Type u} →
  Array α → (cmp : autoParam (α → α → Ordering) Std.ExtTreeMap.unitOfArray._auto_1) → Std.ExtTreeMap α Unit cmp
-- Mathlib.Data.List.Cycle
Cycle.coe_eq_nil : ∀ {α : Type u_1} (l : List α), ↑l = Cycle.nil ↔ l = []
-- Mathlib.RingTheory.Ideal.GoingDown
/-- If for every prime of `S`, the map `Spec Sₚ → Spec Rₚ` is surjective,
the algebra satisfies going down.  -/
Algebra.HasGoingDown.of_comap_localRingHom_surjective : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (∀ (P : Ideal S) [inst_3 : P.IsPrime],
      Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))) →
    Algebra.HasGoingDown R S
-- Mathlib.RingTheory.EssentialFiniteness
/-- A choice of "essential generators" for a ring hom essentially of finite type.
See `Algebra.EssFiniteType.ext`.  -/
RingHom.EssFiniteType.finset : {R : Type u_1} →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → {f : R →+* S} → f.EssFiniteType → Finset S
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.PartialFixpoint.mk : Lean.Syntax → Option Lean.Term → Lean.Elab.PartialFixpointType → Lean.Elab.PartialFixpoint
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.IsFiniteType.finite : ∀ {C : Type u'} {inst : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat}
  {inst_2 : J.WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R} {σ : M.GeneratingSections}
  [self : σ.IsFiniteType], Finite σ.I
-- Mathlib.Analysis.SpecialFunctions.Bernstein
_private.Mathlib.Analysis.SpecialFunctions.Bernstein.0.«term_/ₙ» : Lean.TrailingParserDescr
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppUsing : Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Term) → Lean.MetaM Std.Format
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'.eq_1 : ∀ {n : ℕ} (start len : ℕ) (x : BitVec n), BitVec.extractLsb' start len x = BitVec.ofNat len (x.toNat >>> start)
-- Mathlib.Algebra.BigOperators.Ring.Finset
Int.cast_sum : ∀ {R : Type u_4} {ι : Type u_5} [inst : AddCommGroupWithOne R] (s : Finset ι) (f : ι → ℤ),
  ↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The generalized index of the lattice generated by `I` in the lattice generated by
`𝓞 K` is equal to the norm of the ideal `I`. The result is stated in terms of base change
determinant and is the translation of `NumberField.det_basisOfFractionalIdeal_eq_absNorm` in
the mixed space. This is useful, in particular, to prove that the family obtained from
the `ℤ`-basis of `I` is actually an `ℝ`-basis of the mixed space, see
`fractionalIdealLatticeBasis`.  -/
NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ)
  (e : Module.Free.ChooseBasisIndex ℤ (NumberField.RingOfIntegers K) ≃ Module.Free.ChooseBasisIndex ℤ ↥↑↑I),
  |(NumberField.mixedEmbedding.latticeBasis K).det
        (⇑(NumberField.mixedEmbedding K) ∘ ⇑(NumberField.basisOfFractionalIdeal K I) ∘ ⇑e)| =
    ↑(FractionalIdeal.absNorm ↑I)
-- Lean.Parser.Tactic
Lean.Parser.Tactic.nestedTactic.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↥A.ρ.invariants),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.iCocycles A 0))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesIso₀ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₀ A).inv)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.shortComplexH0 A).f) x)
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.homEquiv_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) (x : { x // P.HasMap x }), P.homEquiv.symm x = P.lift ↑x ⋯
-- Mathlib.Order.RelIso.Basic
RelIso.relEmbeddingCongr_symm_apply_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ ↪r s₂) (a : α₁),
  ((e₁.relEmbeddingCongr e₂).symm f₂) a = e₂.symm (f₂ (e₁ a))
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.nonarchimedean : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ_[p]), ‖q + r‖ ≤ max ‖q‖ ‖r‖
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
/-- If some `r` is strictly larger than the Riemannian edistance between two points, there exists
a path between these two points of length `< r`. Here, we get such a path on `[0, 1]`.
For a more precise version giving locally constant paths around the endpoints, see
`exists_lt_locally_constant_of_riemannianEDist_lt`  -/
Manifold.exists_lt_of_riemannianEDist_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {x y : M} {r : ENNReal},
  Manifold.riemannianEDist I x y < r →
    ∃ γ,
      γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc 0 1) ∧ Manifold.pathELength I γ 0 1 < r
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Condition for `x` being an optimum solution (min) to given `Γ` instance `I`.  -/
ValuedCSP.Instance.IsOptimumSolution : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] → {Γ : ValuedCSP D C} → {ι : Type u_3} → Γ.Instance ι → (ι → D) → Prop
-- Aesop.RuleTac.GoalDiff
/-- Diff two goals.
 -/
Aesop.diffGoals : Lean.MVarId → Lean.MVarId → Aesop.BaseM Aesop.GoalDiff
-- Mathlib.Tactic.Bound.Attribute
/-- Score the type of argument `x`  -/
_private.Mathlib.Tactic.Bound.Attribute.0.Mathlib.Tactic.Bound.typePriority.argPriority : Lean.Expr → Lean.MetaM ℕ
-- Lean.Elab.ConfigEval.DeriveEvalTerm
/-- Wrapper to handle atomic identifiers and dotted identifiers.
 -/
Lean.Elab.ConfigEval.EvalTerm.withSimpleEvalStx : {α : Type} →
  Lean.Name →
    (String → Lean.TSyntaxArray `term → Lean.Elab.TermElabM (α × Lean.Expr)) →
      Lean.Term → Lean.Elab.TermElabM (α × Lean.Expr)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.forget_map : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (A B : Rep.{w, u, v} k G) (f : A ⟶ B),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (Rep.{w, u, v} k G)).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instHasPullbacksEtale : ∀ (X : AlgebraicGeometry.Scheme), CategoryTheory.Limits.HasPullbacks X.Etale
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Nat.toUInt8 5 = 5`
* `Nat.toUInt8 255 = 255`
* `Nat.toUInt8 256 = 0`
* `Nat.toUInt8 259 = 3`
* `Nat.toUInt8 32770 = 2`
 -/
Nat.toUInt8 : ℕ → UInt8
-- Init.Grind.Ordered.Order
Lean.Grind.PartialOrder.le_iff_lt_or_eq : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsPartialOrder α] {a b : α},
  a ≤ b ↔ a < b ∨ a = b
-- Std.Time.Time.Unit.Basic
/-- Converts a `Minute.Offset` to a `Nanosecond.Offset`.
 -/
Std.Time.Nanosecond.Offset.ofMinutes : Std.Time.Minute.Offset → Std.Time.Nanosecond.Offset
-- Mathlib.Order.Heyting.Basic
le_sup_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b ≤ a ⊔ b \ a
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_insert_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m.insert k).size ≤ m.size + 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictAntiOn.mul_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [MulRightStrictMono α], StrictAntiOn f s → ∀ (c : α), StrictAntiOn (fun x => f x * c) s
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Viewing a module as an affine space modelled on itself, we can characterise affine independence
in terms of linear combinations.  -/
affineIndependent_iff : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_5}
  {p : ι → V},
  AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), s.sum w = 0 → ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0
-- Mathlib.InformationTheory.Hamming
Hamming.toHamming_zero : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Zero (β i)], Hamming.toHamming 0 = 0
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.typeDefinitionProvider : Lean.Lsp.ServerCapabilities → Bool
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.map_injective : ∀ {M : Type u_1} [inst : Monoid M] {M' : Type u_3} [inst_1 : Monoid M'] {P : Submonoid M} (e : M →* M'),
  Function.Injective ⇑e → (Submonoid.map e P).FG → P.FG
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Dense.borel_eq_generateFrom_Icc_mem_aux : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α},
  Dense s →
    (∀ (x : α), IsBot x → x ∈ s) →
      (∀ (x y : α), x < y → Set.Ioo x y = ∅ → x ∈ s) →
        borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Set.Icc l u = S}
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instSemilatticeSupFiniteIndexNormalSubgroup : {G : Type u_1} → [inst : Group G] → SemilatticeSup (FiniteIndexNormalSubgroup G)
-- Mathlib.Algebra.Ring.Aut
RingAut.instInhabited : (R : Type u_1) → [inst : Mul R] → [inst_1 : Add R] → Inhabited (RingAut R)
-- Mathlib.GroupTheory.MonoidLocalization.DivPairs
Submonoid.divPairs_comap : ∀ {M : Type u_1} {G : Type u_2} {H : Type u_3} [inst : CommMonoid M] [inst_1 : CommGroup G] [inst_2 : CommGroup H]
  (f : ⊤.LocalizationMap G) (g : ⊤.LocalizationMap H) (s : Submonoid G),
  Submonoid.divPairs g (Submonoid.comap (g.mulEquivOfLocalizations f).toMonoidHom s) = Submonoid.divPairs f s
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.coe_equivToUnitHom : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R') (a : Rˣ),
  ↑((MulChar.equivToUnitHom χ) a) = χ ↑a
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.range_comp_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' F'' : CategoryTheory.Functor C (Type w)} (f : F ⟶ F')
  (g : F' ⟶ F''),
  CategoryTheory.Subfunctor.range (CategoryTheory.CategoryStruct.comp f g) ≤ CategoryTheory.Subfunctor.range g
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_le_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α}, Std.Internal.List.containsKey k l = true → (compare (Std.Internal.List.minKey! l) k).isLE = true
-- Mathlib.RingTheory.Polynomial.Ideal
Polynomial.ker_evalRingHom : ∀ {R : Type u_1} [inst : CommRing R] (x : R),
  RingHom.ker (Polynomial.evalRingHom x) = Ideal.span {Polynomial.X - Polynomial.C x}
-- Mathlib.NumberTheory.NumberField.EquivReindex
NumberField.instInvertibleMatrixRingHomComplexBasisMatrix : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] → [inst_2 : DecidableEq (K →+* ℂ)] → Invertible (NumberField.basisMatrix K)
-- Lean.Meta.Sym.Pattern
/-- Structural definitional equality for applications.
Looks up `ProofInstInfo` for the head constant and delegates to `isDefEqAppWithInfo`
if available, otherwise uses `isDefEqAppDefault`.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqApp : (tFn t : Lean.Expr) → Lean.Expr → tFn = t.getAppFn → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.Analysis.Calculus.AbsolutelyMonotone
/-- A function `f : ℝ → ℝ` is **absolutely monotone on a set `s`** if, heuristically, all
iterated derivatives of `f` on `s` are nonnegative. For technical reasons related to unique
differentiability, the precise definition is phrased as the existence of a Taylor series for
`f` on `s` whose `n`th term, evaluated at the all-ones tuple, is nonnegative for every `n` and
every `x ∈ s`. See `AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg` for the equivalence
under `UniqueDiffOn`.  -/
AbsolutelyMonotoneOn : (ℝ → ℝ) → Set ℝ → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_eraseKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.getValueCast? k (Std.Internal.List.eraseKey k l) = none
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq.injEq : ∀ (c₁ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr)
  (c₁_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (c₂_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.ofLeDiseq c₁_1 c₂_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Std.Time.Time.Unit.Basic
/-- Converts a `Second.Offset` to a `Millisecond.Offset`.
 -/
Std.Time.Second.Offset.toMilliseconds : Std.Time.Second.Offset → Std.Time.Millisecond.Offset
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.image_frontier : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → ∀ (s : Set X), f '' frontier s = frontier (f '' s)
-- Mathlib.Order.Preorder.Chain
isChain_coe_univ_iff : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsChain (fun x1 x2 => r ↑x1 ↑x2) Set.univ ↔ IsChain r s
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.sup : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r r' : α → β → Prop},
  Semicontinuous r → Semicontinuous r' → Semicontinuous (r ⊔ r')
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.instCommRingFiniteAdeleRing : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → CommRing (IsDedekindDomain.FiniteAdeleRing R K)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.monoLM_eq_zero : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E},
  ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂) → ContDiffMapSupportedIn.monoLM 𝕜 = 0
-- Mathlib.Algebra.Order.Monovary
/-- Two functions antivary iff the rearrangement inequality holds.  -/
antivaryOn_iff_mul_rearrangement : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α}
  {s : Set ι}, AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i
-- Mathlib.Analysis.Normed.Group.Constructions
Function.Surjective.pi_norm_comp' : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Fintype ι] [inst_1 : SeminormedGroup E] [inst_2 : Fintype F]
  {f : ι → F}, Function.Surjective f → ∀ (g : F → E), ‖g ∘ f‖ = ‖g‖
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.instInhabited : (α : Type u_2) → [inst : Preorder α] → [inst_1 : AddZeroClass α] → Inhabited (α →+o α)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.in_coverByImage : ∀ {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] (G : CategoryTheory.Functor C D) {X : D} {Y : C} (f : G.obj Y ⟶ X),
  CategoryTheory.Presieve.coverByImage G X f
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_lt : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {k : α → Ordering} [Std.Internal.IsCut compare k]
  {sz : ℕ} {k' : α} {v' : β k'} {l r : Std.DTreeMap.Internal.Impl α β},
  k k' = Ordering.lt →
    (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).Ordered →
      List.filter (fun x => k x.fst == Ordering.lt) (Std.DTreeMap.Internal.Impl.inner sz k' v' l r).toListModel =
        List.filter (fun x => k x.fst == Ordering.lt) l.toListModel ++ ⟨k', v'⟩ :: r.toListModel
-- Mathlib.Data.Int.Bitwise
Int.lor.eq_4 : ∀ (m n : ℕ), (Int.negSucc m).lor (Int.negSucc n) = Int.negSucc (m &&& n)
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instCompleteLattice.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instCompleteLattice =
    { toPartialOrder := inferInstance.toPartialOrder, sup := SemilatticeSup.sup, le_sup_left := ⋯, le_sup_right := ⋯,
      sup_le := ⋯, inf := fun x1 x2 => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯,
      toSupSet := (completeLatticeOfCompleteSemilatticeInf (AddGroupTopology α)).toSupSet, isLUB_sSup := ⋯,
      toInfSet := (completeLatticeOfCompleteSemilatticeInf (AddGroupTopology α)).toInfSet, isGLB_sInf := ⋯,
      toBoundedOrder := inferInstance }
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps.match_1.eq_2 : ∀ {s : String.Slice} (motive : List (String.Slice.Pattern.SearchStep s) → Sort u_1) (startPos endPos : s.Pos)
  (l : List (String.Slice.Pattern.SearchStep s)) (h_1 : Unit → motive [])
  (h_2 :
    (startPos endPos : s.Pos) →
      (l : List (String.Slice.Pattern.SearchStep s)) →
        motive (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l))
  (h_3 :
    (p q : s.Pos) →
      (l : List (String.Slice.Pattern.SearchStep s)) → motive (String.Slice.Pattern.SearchStep.matched p q :: l)),
  (match String.Slice.Pattern.SearchStep.rejected startPos endPos :: l with
    | [] => h_1 ()
    | String.Slice.Pattern.SearchStep.rejected startPos endPos :: l => h_2 startPos endPos l
    | String.Slice.Pattern.SearchStep.matched p q :: l => h_3 p q l) =
    h_2 startPos endPos l
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.symmetrifyQuiver : (V : Type u) → [Quiver V] → Quiver (Quiver.Symmetrify V)
-- Mathlib.Algebra.Group.Commute.Hom
AddSemiconjBy.map : ∀ {F : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Add M] [inst_1 : Add N] {a x y : M} [inst_2 : FunLike F M N]
  [AddHomClass F M N], AddSemiconjBy a x y → ∀ (f : F), AddSemiconjBy (f a) (f x) (f y)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If the coequalizer of two morphisms is a monomorphism, then the two morphisms are equal.  -/
CategoryTheory.Limits.eq_of_mono_coequalizer : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] [CategoryTheory.Mono (CategoryTheory.Limits.coequalizer.π f g)],
  f = g
-- Mathlib.Algebra.Group.Even
IsSquare.eq_1 : ∀ {α : Type u_2} [inst : Mul α] (a : α), IsSquare a = ∃ r, a = r * r
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a function `f`, the smallest additive congruence relation containing the
binary relation on `f`'s image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the
elements of `f⁻¹(y)` by an additive congruence relation `c`.'  -/
AddCon.mapGen : {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → {c : AddCon M} → (M → N) → AddCon N
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.minKey? = some km → t.contains km = true
-- Mathlib.Order.SupIndep
/-- Composing an independent indexed family with an order isomorphism on the elements results in
another independent indexed family.  -/
iSupIndep.map_orderIso : ∀ {ι : Sort u_5} {α : Type u_6} {β : Type u_7} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β)
  {a : ι → α}, iSupIndep a → iSupIndep (⇑f ∘ a)
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.instIsTwoSidedIInf : ∀ {α : Type u} [inst : Semiring α] {ι : Sort u_1} (I : ι → Ideal α) [∀ (i : ι), (I i).IsTwoSided], (⨅ i, I i).IsTwoSided
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.map_le_of_subsingleton : ∀ {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) (f : V ↪ W) [Subsingleton V],
  SimpleGraph.map (⇑f) G ≤ G'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.coreC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (lhs rhs : Lean.Grind.CommRing.Expr) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_certC lhs rhs p c = true →
    Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs →
      Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousWithinAt.rpow_const : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α} {p : ℝ},
  ContinuousWithinAt f s x → f x ≠ 0 ∨ 0 ≤ p → ContinuousWithinAt (fun x => f x ^ p) s x
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_inter_sdiff`. -/
Set.diff_inter_diff : ∀ {α : Type u_1} {s t u : Set α}, s \ t ∩ (s \ u) = s \ (t ∪ u)
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_units_conj' : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸]
  [CompleteSpace 𝔸] (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸),
  NormedSpace.exp (↑U⁻¹ * A * ↑U) = ↑U⁻¹ * NormedSpace.exp A * ↑U
-- Mathlib.Algebra.HierarchyDesign
/-- Certain instances only apply if the goal has a certain shape. For example
`Semiring.toModule [Semiring R] : Module R R` or `Int.instAddGroup : AddGroup ℤ`.
Usually these instances will fail quickly, and when they apply, they are almost always
the desired instance. For performance reasons it is sometimes useful to increase the
priority of these instances, especially if they are defined very early on in mathlib
(which would mean that they would be tried very late if they had the default priority).

Therefore, if we create an instance that only applies in specific circumstances, and that
is essentially always the right answer when it does apply, we may want to set the
priority of these instances to 1100 (or something similar, which is above the default
value of 1000).
 -/
LibraryNote.higher_instance_priority : Batteries.Util.LibraryNote
-- Init.Data.SInt.Bitwise
ISize.zero_shiftLeft : ∀ {a : ISize}, 0 <<< a = 0
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.injective : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), Function.Injective ⇑e
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.isTangent : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → s.IsTangent as
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasPullbacks C}
  {x y : CategoryTheory.Pretopology C}, x.coverings = y.coverings → x = y