mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mem_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N},
  y ∈ AddSubmonoid.map f S ↔ ∃ x ∈ S, f x = y
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem_extract_aux : ∀ {i : ℕ} {xs : ByteArray} {start stop : ℕ}, i < (xs.extract start stop).size → start + i < xs.size
-- Mathlib.Analysis.Complex.AbelLimit
Complex.stolzSet_empty : ∀ {M : ℝ}, M ≤ 1 → Complex.stolzSet M = ∅
-- Mathlib.Util.Superscript
/-- Returns true if every character in `stx : Syntax` can be superscripted
(or subscripted).  -/
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.isValid : Mathlib.Tactic.Superscript.Mapping → Lean.Syntax → Bool
-- Mathlib.Data.Set.Equitable
Set.not_equitableOn : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] [inst_1 : Add β] [inst_2 : One β] {s : Set α} {f : α → β},
  ¬s.EquitableOn f ↔ ∃ a ∈ s, ∃ b ∈ s, f b + 1 < f a
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.eventually_imp : ∀ {α : Type u} {f : Ultrafilter α} {p q : α → Prop},
  (∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_mulVec_repr : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) [inst_3 : Fintype ι] [Finite ι'] (m : M),
  (b'.toMatrix ⇑b).mulVec ⇑(b.repr m) = ⇑(b'.repr m)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- Given a natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of arbitrary category,
where `G` is locally-full and cover-dense, and `ℱ'` is a sheaf, we may obtain a natural
transformation between presheaves.
 -/
CategoryTheory.Functor.IsCoverDense.sheafHom : {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] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {A : Type u_4} →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
              {G : CategoryTheory.Functor C D} →
                [G.IsCoverDense K] →
                  [G.IsLocallyFull K] →
                    {ℱ : CategoryTheory.Functor Dᵒᵖ A} →
                      {ℱ' : CategoryTheory.Sheaf K A} → (G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) → (ℱ ⟶ ℱ'.obj)
-- Mathlib.Data.Set.Basic
Set.MemUnion.elim : ∀ {α : Type u} {x : α} {a b : Set α} {P : Prop}, x ∈ a ∪ b → (x ∈ a → P) → (x ∈ b → P) → P
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.diagonal_vec3 : ∀ {α : Type u} [inst : Zero α] (a b c : α), Matrix.diagonal ![a, b, c] = !![a, 0, 0; 0, b, 0; 0, 0, c]
-- Mathlib.Algebra.Ring.Hom.Defs
/-- `f : α →+* β` doesn't map `1` to `0` if `β` is nontrivial  -/
RingHom.map_one_ne_zero : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) [Nontrivial β],
  f 1 ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.GroupSMul.linearMap_apply : ∀ (R : Type u_1) {M : Type u_7} [inst : Monoid M] [inst_1 : CommSemiring R] (V : Type u_10) [inst_2 : AddCommMonoid V]
  [inst_3 : Module R V] [inst_4 : Module (MonoidAlgebra R M) V] [inst_5 : IsScalarTower R (MonoidAlgebra R M) V] (g : M)
  (v : V), (MonoidAlgebra.GroupSMul.linearMap R V g) v = MonoidAlgebra.single g 1 • v
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Module.lift_of : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Semiring R]
  [inst_5 : (i : ι) → AddCommMonoid (G i)] [inst_6 : (i : ι) → Module R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] {P : Type u_7}
  [inst_9 : AddCommMonoid P] [inst_10 : Module R P] (g : (i : ι) → G i →ₗ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι} (x : G i),
  (DirectLimit.Module.lift R ι G f g Hg) ((DirectLimit.Module.of R ι G f i) x) = (g i) x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1π.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.H1π A = CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₁ A).inv (groupHomology.π A 1)
-- Mathlib.Analysis.Normed.Group.Pointwise
inv_thickening : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E), (Metric.thickening δ s)⁻¹ = Metric.thickening δ s⁻¹
-- Mathlib.Topology.Bases
/-- Any open set is the union of the basis sets contained in it.  -/
TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' : ∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis B → ∀ {u : Set α}, IsOpen u → u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.IsOneHypercoverDense.mk : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C},
  (∀ (X : C), Nonempty (F.OneHypercoverDenseData J₀ J X)) → F.IsOneHypercoverDense J₀ J
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.le_of_le_cert.match_1.eq_3 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (c₁ c₂ : ℤ)
  (h_1 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k_1 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1))
  (h_2 :
    (k k_1 : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p))
  (h_3 : (c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)),
  (match Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ with
    | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_1 => h_1 k v p k_1
    | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_1 v p => h_2 k k_1 v p
    | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => h_3 c₁ c₂
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_3 c₁ c₂
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.neg.inj : ∀ {a a_1 : ℕ}, Sat.Literal.neg a = Sat.Literal.neg a_1 → a = a_1
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.eq_zero_of_aeval_eq_zero : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A], AlgebraicIndependent R x → ∀ (p : MvPolynomial ι R), (MvPolynomial.aeval x) p = 0 → p = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.rightOp_right_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  {X_1 Y : SimplexCategory} (f : X_1 ⟶ Y), X.rightOp.right.map f = (X.left.map f.op).op
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.mulR.injEq : ∀ (a : Int.Internal.Linear.Expr) (k : ℤ) (a_1 : Int.Internal.Linear.Expr) (k_1 : ℤ),
  (a.mulR k = a_1.mulR k_1) = (a = a_1 ∧ k = k_1)
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.const.get_mk : ∀ {n : ℕ} {A : Type u} {α : TypeVec.{u} n} (x : A), MvPFunctor.const.get (MvPFunctor.const.mk n x) = x
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.aeval_coe_eq_smeval : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : Algebra R S] (x : S),
  ⇑(Polynomial.aeval x) = fun p => p.smeval x
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The identity over `X` is terminal.  -/
CategoryTheory.Over.mkIdTerminal : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Limits.IsTerminal (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id X))
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearMap.integral_comp_comm' : ∀ {X : Type u_1} {E : Type u_3} {Fₗ : Type u_5} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  [inst_1 : RCLike 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedAddCommGroup Fₗ]
  [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace ℝ Fₗ] [CompleteSpace Fₗ] [inst_8 : NormedSpace ℝ E]
  [CompleteSpace E] (L : E →L[𝕜] Fₗ) {K : NNReal},
  AntilipschitzWith K ⇑L → ∀ (φ : X → E), ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `repr` preserves zero, up to multiples of `f`  -/
IsAdjoinRoot.repr_zero_mem_span : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), h.repr 0 ∈ Ideal.span {f}
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.snd_comp_inr : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  (AddMonoidHom.snd M N).comp (AddMonoidHom.inr M N) = AddMonoidHom.id N
-- Mathlib.Data.EReal.Basic
EReal.natCast_ne_iff : ∀ {m n : ℕ}, ↑m ≠ ↑n ↔ m ≠ n
-- Mathlib.Algebra.Group.Conj
AddConjClasses.quot_mk_eq_mk : ∀ {α : Type u} [inst : AddMonoid α] (a : α), Quot.mk (⇑(IsAddConj.setoid α)) a = AddConjClasses.mk a
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.condition_assoc : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.add_zsmul : ∀ {ι : 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} {b : P.Base}
  [inst_5 : CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i j k : ι} {z : ℤ},
  i ≠ j → b.IsPos i → j ∈ b.support → P.root k = P.root i + z • P.root j → b.IsPos k
-- Lean.Elab.Level
Lean.Elab.Level.Context.autoBoundImplicit : Lean.Elab.Level.Context → Bool
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.oset.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {i : ℕ} {y : Lean.Compiler.LCNF.Arg pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_3} {fvarId_1 : Lean.FVarId}
  {i_1 : ℕ} {y_1 : Lean.Compiler.LCNF.Arg pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_3},
  Lean.Compiler.LCNF.CodeDecl.oset fvarId i y h = Lean.Compiler.LCNF.CodeDecl.oset fvarId_1 i_1 y_1 h_1 →
    fvarId = fvarId_1 ∧ i = i_1 ∧ y = y_1
-- Mathlib.Probability.Independence.Basic
/-- Given random variables `X : Ω → 𝓧` and `Y : Ω' → 𝓨`, they are independent when viewed as random
variables defined on the product space `Ω × Ω'`.  -/
ProbabilityTheory.indepFun_prod₀ : ∀ {Ω : Type u_10} {Ω' : Type u_11} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω}
  {ν : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  {𝓧 : Type u_12} {𝓨 : Type u_13} [inst : MeasurableSpace 𝓧] [inst_1 : MeasurableSpace 𝓨] {X : Ω → 𝓧} {Y : Ω' → 𝓨},
  AEMeasurable X μ → AEMeasurable Y ν → ProbabilityTheory.IndepFun (fun ω => X ω.1) (fun ω => Y ω.2) (μ.prod ν)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α} {fallback : Unit},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.insertManyIfNewUnit m l) k fallback = ()
-- Mathlib.Topology.Algebra.Group.Basic
Filter.neg_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, -nhdsWithin a (Set.Iio a) = nhdsWithin (-a) (Set.Ioi (-a))
-- Mathlib.SetTheory.Ordinal.Enum
Ordinal.enumOrd_surjective : ∀ {s : Set Ordinal.{u}}, ¬BddAbove s → ∀ {b : Ordinal.{u}}, b ∈ s → ∃ a, Ordinal.enumOrd s a = b
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHomMonomial_single_one : ∀ {σ : Type u_1} {R : Type u_3} {n k : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] {i : Fin n},
  MvPolynomial.esymmAlgHomMonomial σ (fun₀ | i => k) 1 = MvPolynomial.esymm σ R (↑i + 1) ^ k
-- Mathlib.Data.Finset.Prod
/-- The number of strictly ordered pairs `(a, b)` with `a, b ∈ s` is `(#s).choose 2`.  -/
Finset.card_product_filter_lt : ∀ {α : Type u_1} {s : Finset α} [inst : LinearOrder α], {x ∈ s ×ˢ s | x.1 < x.2}.card = s.card.choose 2
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.toAddEquiv_eq_coe : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S'), equiv.toAddEquiv = ↑equiv
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
/-- The `circleAverage (log ‖· + a‖) 0 1` equals `log⁺ ‖a‖`.
 -/
circleAverage_log_norm_add_const_eq_posLog : ∀ {a : ℂ}, Real.circleAverage (fun x => Real.log ‖x + a‖) 0 1 = ‖a‖.posLog
-- Mathlib.Data.Int.Init
Int.toNat_lt_of_ne_zero : ∀ {m : ℤ} {n : ℕ}, n ≠ 0 → (m.toNat < n ↔ m < ↑n)
-- Mathlib.GroupTheory.Index
Subgroup.index_map_of_injective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) {f : G →* G'},
  Function.Injective ⇑f → (Subgroup.map f H).index = H.index * f.range.index
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_s : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).s = f ((CategoryTheory.Limits.pullback.fst f g) t)
-- Init.Data.String.Basic
String.str_sliceFrom : ∀ {s : String} {p : s.Pos}, (s.sliceFrom p).str = s
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Given bases of two modules `M₁` and `M₂` over a commutative ring `R`, we get a linear
equivalence between matrices over `R` indexed by the bases and linear maps `M₁ →ₗ M₂`.  -/
Matrix.toLin : {R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_3} →
      {n : Type u_4} →
        [Fintype n] →
          [Finite m] →
            [DecidableEq n] →
              {M₁ : Type u_5} →
                {M₂ : Type u_6} →
                  [inst_4 : AddCommMonoid M₁] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module R M₂] →
                          Module.Basis n R M₁ → Module.Basis m R M₂ → Matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂
-- Mathlib.Data.List.Perm.Basic
List.set_perm_cons_eraseIdx : ∀ {α : Type u_1} {l : List α} {n : ℕ}, n < l.length → ∀ (a : α), (l.set n a).Perm (a :: l.eraseIdx n)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.addMonoid : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → AddMonoid (TensorProduct R M N)
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` is continuous.  -/
Real.continuous_posLog : Continuous Real.posLog
-- Std.Data.DTreeMap.Raw.Iterator
/-- Returns a finite iterator over the keys of a dependent tree map.
The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DTreeMap.Raw.keysIter : {α : Type u} → {β : α → Type u} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Std.Iter α
-- Mathlib.Algebra.Group.Opposite
AddOpposite.addCommute_op : ∀ {α : Type u_1} [inst : Add α] {x y : α}, AddCommute (AddOpposite.op x) (AddOpposite.op y) ↔ AddCommute x y
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  (m.insert k).contains a = (k == a || m.contains a)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_single_index : ∀ (α : Type u_1) (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (c : M) (a : α) (f : α →₀ R) [inst_3 : DecidableEq α], (Finsupp.linearCombination R (Pi.single a c)) f = f a • c
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Mon (CategoryTheory.Comon C)),
  (CategoryTheory.Bimon.equivMonComonCounitIsoApp M).inv.hom.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Std.Do.SPred.Laws
Std.Do.SPred.exists_intro : ∀ {σs : List (Type u)} {α : Sort u_1} {Ψ : α → Std.Do.SPred σs} (a : α), Ψ a ⊢ₛ ∃ a, Ψ a
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_codRestrict : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {S : Type u_8} [inst_2 : SetLike S N]
  [inst_3 : SubmonoidClass S N] (f : G →* N) (s : S) (h : ∀ (x : G), f x ∈ s), (f.codRestrict s h).ker = f.ker
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
/-- `LiouvilleNumber.partialSum` is the sum of the first `k + 1` terms of Liouville's constant,
i.e.
$$
\sum_{i=0}^k\frac{1}{m^{i!}}.
$$
 -/
LiouvilleNumber.partialSum : ℝ → ℕ → ℝ
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompIso_hom_app : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  {F₀₁ : CategoryTheory.Functor C₀ C₁} {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀) (X : C₀),
  (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).hom.app X =
    CategoryTheory.CategoryStruct.comp (F₁₂.map (F₀₁.map (adj₀₂.unit.app X)))
      (CategoryTheory.CategoryStruct.comp (F₁₂.map (F₀₁.map (e₀₁₂.inv.app (F₀₂.obj X))))
        (CategoryTheory.CategoryStruct.comp (F₁₂.map (adj₀₁.counit.app (G₂₁.obj (F₀₂.obj X))))
          (adj₁₂.counit.app (F₀₂.obj X))))
-- Mathlib.LinearAlgebra.Orientation
/-- A module is canonically oriented with respect to an empty index type.  -/
IsEmpty.oriented : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → (ι : Type u_4) → [IsEmpty ι] → Module.Oriented R M ι
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `≤` on `BitVec`s.  -/
BitVec.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- When `f` is an isomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `g`.
 -/
CategoryTheory.Limits.kernelIsIsoComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            [inst_2 : CategoryTheory.IsIso f] →
              [inst_3 : CategoryTheory.Limits.HasKernel g] →
                CategoryTheory.Limits.kernel (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.Limits.kernel g
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.surj'' : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (z : S), ∃ r m, z = r • ↑((IsLocalization.toInvSubmonoid M S) m)
-- Lean.Elab.Command
Lean.Elab.Command.Context.fileMap : Lean.Elab.Command.Context → Lean.FileMap
-- Mathlib.Algebra.Ring.Defs
Semiring.toNonUnitalSemiring : {α : Type u} → [self : Semiring α] → NonUnitalSemiring α
-- Init.Grind.Attr
/-- The `→` modifier instructs `grind` to select a multi-pattern from the hypotheses of the theorem.
In other words, `grind` will use the theorem for forwards reasoning.
To generate a pattern, it traverses the hypotheses of the theorem from left to right.
Each time it encounters a subexpression which covers an argument which was not
previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
Lean.Parser.Attr.grindFwd : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.empty_eq : ∀ {α : Type u} {β : α → Type v} {c : ℕ},
  Std.DHashMap.Raw.emptyWithCapacity c = ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity c)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Int.addSubgroupClosure_one : AddSubgroup.closure {1} = ⊤
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMapWithin_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {X : TangentSpace I x}, (tangentMapWithin I I' f s ⟨x, X⟩).snd = (mfderiv[s] f x) X
-- Mathlib.CategoryTheory.GlueData
/-- The constructed `GlueData` of a `GlueData'`, where `GlueData'` is a variant of `GlueData` that only
requires conditions on `V (i, j)` when `i ≠ j`.
 -/
CategoryTheory.GlueData.ofGlueData' : {C : Type u₁} → [inst : CategoryTheory.Category.{v, u₁} C] → CategoryTheory.GlueData' C → CategoryTheory.GlueData C
-- Aesop.Builder.Basic
Aesop.instInhabitedRuleBuilderInput : Inhabited Aesop.RuleBuilderInput
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_eq_getD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  (fallback : β) {h : a ∈ t}, t[a] = t.getD a fallback
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup G} {K : Subgroup N},
  H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.coe_comp_continuousOrderHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  (g : EsakiaHom β γ) (f : EsakiaHom α β), ↑(g.comp f) = (↑g).comp ↑f
-- Mathlib.Analysis.Complex.CoveringMap
Complex.isQuotientCoveringMap_npow : ∀ (n : ℕ) [NeZero n], IsQuotientCoveringMap (fun z => z ^ n) ↥(powMonoidHom n).ker
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_X_comp_const : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {f : PowerSeries R} {i : τ},
  MvPowerSeries.subst (MvPowerSeries.X ∘ fun x => i) f = PowerSeries.subst (MvPowerSeries.X i) f