mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Vector.Basic
List.Vector.mmap_cons : ∀ {m : Type u_6 → Type u_7} [inst : Monad m] {α : Type u_8} {β : Type u_6} (f : α → m β) (a : α) {n : ℕ}
  (v : List.Vector α n),
  List.Vector.mmap f (a ::ᵥ v) = do
    let h' ← f a
    let t' ← List.Vector.mmap f v
    pure (h' ::ᵥ t')
-- Mathlib.Data.Stream.Init
Stream'.mem_append_stream_right : ∀ {α : Type u} {a : α} (l : List α) {s : Stream' α}, a ∈ s → a ∈ l ++ₛ s
-- Std.Data.ExtTreeSet.Basic
/-- Monadically computes a value by folding the given function over the elements in the tree set in
ascending order.
 -/
Std.ExtTreeSet.foldlM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} →
      {m : Type w → Type w₂} →
        [inst : Monad m] → [LawfulMonad m] → [Std.TransCmp cmp] → (δ → α → m δ) → δ → Std.ExtTreeSet α cmp → m δ
-- Mathlib.Analysis.Convex.Function
convexOn_iff_convex_epigraph : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulMono 𝕜 β] {s : Set E} {f : E → β}, ConvexOn 𝕜 s f ↔ Convex 𝕜 {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.coe_mk_nonempty_iff : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {i : ιₚ}
  (g : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i)).subtype (↑ps i).symmetries),
  (↑{ index := i, groupElts := g }).Nonempty ↔ (↑(↑ps i)).Nonempty
-- Mathlib.Order.BooleanAlgebra.Defs
/-- The supremum of `x` and `xᶜ` is at least `⊤`  -/
BooleanAlgebra.top_le_sup_compl : ∀ {α : Type u} [self : BooleanAlgebra α] (x : α), ⊤ ≤ x ⊔ xᶜ
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toStarAlgHom_ofStarAlgHom : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] [inst_5 : Star A₁] [inst_6 : Star A₂] (f : A₁ →⋆ₐ[R] A₂)
  (g : A₂ →⋆ₐ[R] A₁) (h₁ : g.comp f = StarAlgHom.id R A₁) (h₂ : f.comp g = StarAlgHom.id R A₂),
  (StarAlgEquiv.ofStarAlgHom f g h₁ h₂).toStarAlgHom = f
-- Mathlib.Probability.Process.HittingTime
/-- **Alias** of `MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime`.

---

The hitting time of a discrete process with the starting time indexed by a stopping time
is a stopping time.  -/
MeasureTheory.isStoppingTime_hittingBtwn_isStoppingTime : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [WellFoundedLT ι] [Countable ι] [inst_3 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
  [inst_6 : MeasurableSpace β] {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {τ : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ →
    ∀ {N : ι},
      (∀ (x : Ω), τ x ≤ ↑N) →
        ∀ {s : Set β},
          MeasurableSet s →
            MeasureTheory.Adapted f u →
              MeasureTheory.IsStoppingTime f fun x => ↑(MeasureTheory.hittingBtwn u s (τ x).untopA N x)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {k : α} {v : β k}, (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v
-- Mathlib.Order.WithBot
WithTop.forall_le_coe : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {p : WithTop α → Prop}, (∀ x ≤ ↑a, p x) ↔ ∀ b ≤ a, p ↑b
-- Std.Http.Data.Body.Stream
/-- Closes the channel.
 -/
Std.Http.Body.Stream.close : Std.Http.Body.Stream → Std.Async.Async Unit
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.iInf_adj : ∀ {ι : Sort u_1} {V : Type u} {a b : V} {f : ι → SimpleGraph V}, (⨅ i, f i).Adj a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ a ≠ b
-- Mathlib.Topology.Sequences
SequentialSpace.iSup : ∀ {X : Type u_4} {ι : Sort u_3} {t : ι → TopologicalSpace X}, (∀ (i : ι), SequentialSpace X) → SequentialSpace X
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_Ioo : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrder α] (a b : α), (Set.Ioo a b).Finite
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
AddAction.IsMultiplyPreprimitive.mk : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {n : ℕ},
  AddAction.IsMultiplyPretransitive M α n →
    (∀ {s : Set α},
        s.encard + 1 = ↑n → AddAction.IsPreprimitive ↥(fixingAddSubgroup M s) ↥(SubAddAction.ofFixingAddSubgroup M s)) →
      AddAction.IsMultiplyPreprimitive M α n
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.congrOrderIso.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N]
  (e : MulArchimedeanClass M ≃o MulArchimedeanClass N),
  FiniteMulArchimedeanClass.congrOrderIso e = { toEquiv := (↑e).subtypeEquiv ⋯, map_rel_iff' := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = false → (m₁.diff m₂).getKey? k = m₁.getKey? k
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- A monad equipped with the ability to construct `Mor₂Iso` terms.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso : (Type → Type) → Type
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.SupportsStmt.match_1.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q))
  (h_2 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) (h_7 : Unit → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.branch a q₁ q₂ with
    | Turing.TM2.Stmt.push k a q => h_1 k a q
    | Turing.TM2.Stmt.peek k a q => h_2 k a q
    | Turing.TM2.Stmt.pop k a q => h_3 k a q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | Turing.TM2.Stmt.goto l => h_6 l
    | Turing.TM2.Stmt.halt => h_7 ()) =
    h_5 a q₁ q₂
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.snd.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.snd M N = { toFun := Prod.snd, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Field.Periodic
Function.Periodic.const_inv_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (a⁻¹ * x)) (a * c)
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- `G.neighborSet v` is the set of vertices adjacent to `v` in `G`.  -/
SimpleGraph.neighborSet : {V : Type u} → SimpleGraph V → V → Set V
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.mulSupport_one_add : ∀ {ι : Type u_1} {R : Type u_5} [inst : One R] [inst_1 : AddLeftCancelMonoid R] (f : ι → R),
  (Function.mulSupport fun x => 1 + f x) = Function.support f
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_monomial : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R), ((Polynomial.monomial n) r).toFinsupp = AddMonoidAlgebra.single n r
-- Mathlib.Order.Antichain
IsAntichain.image : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsAntichain r s → ∀ (f : α → β), (∀ ⦃a b : α⦄, r' (f a) (f b) → r a b) → IsAntichain r' (f '' s)
-- Mathlib.Topology.Category.Compactum
/-- The functor `compactumToCompHaus` is full.  -/
compactumToCompHaus.full : compactumToCompHaus.Full
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_rightUnitor_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  Bicategory.Opposite.op2 (CategoryTheory.Bicategory.rightUnitor f).inv =
    (CategoryTheory.Bicategory.leftUnitor f.op).inv
-- Mathlib.Topology.Algebra.ProperConstSMul
instProperConstVAddOfContinuousConstVAdd : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace X]
  [ContinuousConstVAdd G X], ProperConstVAdd G X
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.NullMeasurableSet.prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {s : Set α} {t : Set β},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.NullMeasurableSet t ν → MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν)
-- Mathlib.Computability.Language
Language.instMembershipList : {α : Type u_1} → Membership (List α) (Language α)
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
/-- The double commutant definition of a von Neumann algebra,
as a \*-closed subalgebra of bounded operators on a Hilbert space,
which is equal to its double commutant.

Note that this definition is parameterised by the Hilbert space
on which the algebra faithfully acts, as is standard in the literature.
See `WStarAlgebra` for the abstract notion (a C⋆-algebra with Banach space predual).

Note this is a bundled structure, parameterised by the Hilbert space `H`,
rather than a typeclass on the type of elements.
Thus we can't say that the bounded operators `H →L[ℂ] H` form a `VonNeumannAlgebra`
(although we will later construct the instance `WStarAlgebra (H →L[ℂ] H)`),
and instead will use `⊤ : VonNeumannAlgebra H`.
 -/
VonNeumannAlgebra : (H : Type u) → [inst : NormedAddCommGroup H] → [InnerProductSpace ℂ H] → [CompleteSpace H] → Type u
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.mem_oneLE : ∀ {H : Type u_1} [inst : CommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedMonoid H] {a : H},
  a ∈ GroupCone.oneLE H ↔ 1 ≤ a
-- Init.Data.UInt.Lemmas
USize.toUInt16_eq : ∀ (a b : USize), a.toUInt16 = b.toUInt16 ↔ a % 65536 = b % 65536
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  [inst_8 : DecidableEq ι] (f : F [⋀^ι]→L[𝕜] G) (g dg : E →L[𝕜] F) (v : ι → E),
  ((f.fderivCompContinuousLinearMap g) dg) v = ∑ i, f fun j => (Function.update (fun x => g) i dg j) (v j)
-- Lean.Data.PersistentArray
_private.Lean.Data.PersistentArray.0.Lean.PersistentArray.forFromMAux : {α : Type u} →
  {m : Type v → Type w} →
    [Monad m] → (α → m PUnit.{v + 1}) → Lean.PersistentArrayNode α → USize → USize → m PUnit.{v + 1}
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.mul_antipode_lTensor_comul_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (a : A),
  (LinearMap.mul' R A) ((LinearMap.lTensor A (HopfAlgebraStruct.antipode R)) (CoalgebraStruct.comul a)) =
    (algebraMap R A) (CoalgebraStruct.counit a)
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The value of `f` at the cusp `∞` (or an arbitrary choice of value if this limit is not
well-defined).  -/
UpperHalfPlane.valueAtInfty : (UpperHalfPlane → ℂ) → ℂ
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.parseLowerHex?.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (h_1 : (d : ℕ) → motive (some d)) (h_2 : Unit → motive none),
  (match none with
    | some d => h_1 d
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection has norm `≤ 1`.  -/
Submodule.orthogonalProjectionOnto_norm_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], ‖K.orthogonalProjectionOnto‖ ≤ 1
-- Mathlib.Data.Finset.Max
Finset.max_eq_bot : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α}, s.max = ⊥ ↔ s = ∅
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalBoolExpr : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Computability.DFA
DFA.eval_singleton : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) (a : α), M.eval [a] = M.step M.start a
-- Mathlib.CategoryTheory.Localization.LocallySmall
/-- If `L : C ⥤ D` is a localization functor for a class of morphisms
`W : MorphismProperty C`, and `D` is locally `w`-small, we may obtain
a `HasLocalization.{w} W` instance by shrinking the morphisms in `D`.
(This version assumes that the types of objects of the categories
`C` and `D` are in the same universe.)  -/
CategoryTheory.MorphismProperty.hasLocalizationOfLocallySmall : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {D : Type u₁} →
        [inst_1 : CategoryTheory.Category.{v₂, u₁} D] →
          [CategoryTheory.LocallySmall.{w, v₂, u₁} D] →
            (L : CategoryTheory.Functor C D) → [L.IsLocalization W] → W.HasLocalization
-- Mathlib.Order.Bounds.Basic
BddAbove.insert : ∀ {α : Type u_1} [inst : Preorder α] [IsDirectedOrder α] {s : Set α} (a : α), BddAbove s → BddAbove (insert a s)
-- Mathlib.Data.Set.Defs
/-- The union of two sets `s` and `t` is the set of elements contained in either `s` or `t`.

Note that you should **not** use this definition directly, but instead write `s ∪ t`.  -/
Set.union : {α : Type u} → Set α → Set α → Set α
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- The `K`-sheafification of a family of sets `𝒮` in `F`: If `F` is
a sheaf for `K`, this is the smallest subsheaf of `F` containing `𝒮`.  -/
CategoryTheory.Precoverage.subsheafify : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Precoverage C →
      {F : CategoryTheory.Functor Cᵒᵖ (Type w)} → ((Z : C) → Set (F.obj (Opposite.op Z))) → CategoryTheory.Subfunctor F
-- Mathlib.Control.Monad.Cont
StateT.callCC : {m : Type u → Type v} →
  {σ : Type u} → [MonadCont m] → {α β : Type u} → (MonadCont.Label α (StateT σ m) β → StateT σ m α) → StateT σ m α
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mk : {K : Type u} →
  [inst : DivisionRing K] → (toSubring : Subring K) → (∀ x ∈ toSubring.carrier, x⁻¹ ∈ toSubring.carrier) → Subfield K
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_one : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [inst_1 : One β], AEMeasurable (fun x => 1) μ
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.linearIndependent_of_sub_mem_range_root : ∀ {ι : 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) [CharZero R]
  [IsAddTorsionFree M] [P.IsReduced] {i j : ι},
  P.root i - P.root j ∈ Set.range ⇑P.root → LinearIndependent R ![P.root i, P.root j]
-- Mathlib.Order.Hom.Basic
OrderIso.coe_toOrderEmbedding : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), ⇑e.toOrderEmbedding = ⇑e
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.map_ne_zero_iff : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R ≃+* S) {x : R}, f x ≠ 0 ↔ x ≠ 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
/-- Auxiliary definition for `tensorObj`.  -/
PresheafOfModules.Monoidal.tensorObjMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
      (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) →
        {X Y : Cᵒᵖ} →
          (f : X ⟶ Y) →
            CategoryTheory.MonoidalCategoryStruct.tensorObj (M₁.obj X) (M₂.obj X) ⟶
              (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj
                (CategoryTheory.MonoidalCategoryStruct.tensorObj (M₁.obj Y) (M₂.obj Y))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMaxEntry?_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Internal.Impl.Const.maxEntry? t₁ = Std.DTreeMap.Internal.Impl.Const.maxEntry? t₂
-- Mathlib.Algebra.GroupWithZero.Commute
Commute.inv_right_iff₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {a b : G₀}, Commute a b⁻¹ ↔ Commute a b
-- Mathlib.Order.Hom.Lattice
InfHom.inf_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : SemilatticeInf β] (f g : InfHom α β) (a : α),
  (f ⊓ g) a = f a ⊓ g a
-- Mathlib.CategoryTheory.Filtered.FinallySmall
CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_3 : CategoryTheory.FinallySmall C],
  CategoryTheory.IsFiltered (CategoryTheory.FinallySmall.FilteredFinalModel C)
-- Init.Data.UInt.Basic
instShiftLeftUInt64 : ShiftLeft UInt64
-- Mathlib.Data.Prod.Basic
Prod.swap_injective : ∀ {α : Type u_1} {β : Type u_2}, Function.Injective Prod.swap
-- Init.Data.Random
/-- Returns a pseudorandom number between `lo` and `hi`, using and updating a saved random generator
state.

This state can be seeded using `IO.setRandSeed`.
 -/
IO.rand : ℕ → ℕ → BaseIO ℕ
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.centralizer_center : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.centralizer ↑(AddSubgroup.center G) = ⊤
-- Mathlib.Data.Set.Semiring
SetSemiring.mulLeftMono : ∀ {α : Type u_1} [inst : Mul α], MulLeftMono (SetSemiring α)
-- Aesop.Frontend.Saturate
Aesop.Frontend.evalSaturate : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_le_abs_of_nonneg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a b : α} [AddLeftMono α], 0 ≤ a → a ≤ b → |a| ≤ |b|
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.mul_right_cancel_iff' : ∀ {a b c m : ℕ}, c ≠ 0 → (a * c ≡ b * c [MOD m * c] ↔ a ≡ b [MOD m])
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.isScalarTower : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α β] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [IsScalarTower α β γ], IsScalarTower α β (Set γ)
-- Init.Data.List.Monadic
List.mapM_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [inst : Monad m] [LawfulMonad m]
  {f : α → m β},
  List.mapM f (a :: l) = do
    let __do_lift ← f a
    let __do_lift_1 ← List.mapM f l
    pure (__do_lift :: __do_lift_1)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- A function `f : X → E` is *locally integrable on s*, for `s ⊆ X`, if for every `x ∈ s` there is
a neighbourhood of `x` within `s` on which `f` is integrable.

Note that this is, in general, strictly weaker than local integrability with respect to
`μ.restrict s`. For example, `fun (x : ℝ) ↦ 1/x` is locally integrable on `Set.Ioo 0 1` with
respect to the Lebesgue measure, but it is *not* locally integrable with respect to the
Lebesgue measure restricted to `Set.Ioo 0 1`.  -/
MeasureTheory.LocallyIntegrableOn : {X : Type u_1} →
  {ε : Type u_3} →
    [inst : MeasurableSpace X] →
      [TopologicalSpace X] →
        [inst_2 : TopologicalSpace ε] →
          [ContinuousENorm ε] →
            (X → ε) → Set X → autoParam (MeasureTheory.Measure X) MeasureTheory.LocallyIntegrableOn._auto_1 → Prop
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.sum_digits_ofDigits_eq_sum : ∀ {b : ℕ},
  1 < b → ∀ {l : ℕ} {L : List ℕ}, L ∈ {L | L.length = l ∧ ∀ x ∈ L, x < b} → (b.digits (Nat.ofDigits b L)).sum = L.sum
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.add : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M N : Matrix m m R} {b : m → α} [inst : LT α] [inst_1 : AddZeroClass R],
  M.BlockTriangular b → N.BlockTriangular b → (M + N).BlockTriangular b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesCokernel.iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f] [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G],
  (CategoryTheory.Limits.PreservesCokernel.iso G f).inv = CategoryTheory.Limits.cokernelComparison f G
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree has size at least `lb`.  -/
Std.DTreeMap.Internal.Impl.SizedBalancedTree.lb_le_size_impl : ∀ {α : Type u} {β : α → Type v} {lb ub : ℕ} (self : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β lb ub),
  lb ≤ self.impl.size
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
/-- The composition of bundled affine maps between convex spaces.  -/
Convexity.ConvexSpace.AffineMap.comp : {R : Type u_1} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        {X : Type u_2} →
          {Y : Type u_3} →
            {Z : Type u_4} →
              [inst_3 : Convexity.ConvexSpace R X] →
                [inst_4 : Convexity.ConvexSpace R Y] →
                  [inst_5 : Convexity.ConvexSpace R Z] →
                    Convexity.ConvexSpace.AffineMap R Y Z →
                      Convexity.ConvexSpace.AffineMap R X Y → Convexity.ConvexSpace.AffineMap R X Z
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_fun_bijective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [Finite ι],
  Function.Bijective ⇑(dualTensorHom R M N) → Function.Bijective ⇑(dualTensorHom R M (ι → N))
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unoneD_eq_self_iff : ∀ {α : Type u} {d : α} {x : WithOne α}, WithOne.unoneD d x = d ↔ x = ↑d ∨ x = 1
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.leadingCoeff_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.leadingCoeff ≠ 0 ↔ p ≠ 0
-- Mathlib.Topology.Algebra.GroupWithZero
tendsto_inv₀ : ∀ {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀] {x : G₀},
  x ≠ 0 → Filter.Tendsto Inv.inv (nhds x) (nhds x⁻¹)
-- Init.Grind.Ring.Field
/-- An exponentiation operator.  -/
Lean.Grind.Field.zpow : {α : Type u} → [self : Lean.Grind.Field α] → HPow α ℤ α
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.smulFamily.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid V] [inst_3 : SMulWithZero R V] (f : α → R) (s : HahnSeries.SummableFamily Γ V α),
  HahnSeries.SummableFamily.smulFamily f s =
    { toFun := fun a => f a • s a, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }
-- Lean.Server.Completion.SyntheticCompletion
/-- If there are `Info`s that contain `hoverPos` and have a nonempty `LocalContext`,
yields the closest one of those `Info`s.
Otherwise, yields the closest `Info` that contains `hoverPos` and has an empty `LocalContext`.
 -/
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findClosestInfoWithLocalContextAt? : String.Pos.Raw → Lean.Elab.InfoTree → Option (Lean.Elab.ContextInfo × Lean.Elab.Info)