mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.BoolRing
BoolRing.hasForgetToBoolAlg_forget₂_map : ∀ {X Y : BoolRing} (f : X ⟶ Y), CategoryTheory.HasForget₂.forget₂.map f = BoolAlg.ofHom (BoolRing.Hom.hom f).asBoolAlg
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftBindFunction.liftBind_pure : ∀ {m : Type u → Type v} {n : Type w → Type x} {inst : Monad m} {inst_1 : Monad n}
  {liftBind : (γ : Type u) → (δ : Type w) → (γ → n δ) → m γ → n δ}
  [self : Std.Internal.LawfulMonadLiftBindFunction liftBind] {γ : Type u} {δ : Type w} (f : γ → n δ) (a : γ),
  liftBind γ δ f (pure a) = f a
-- Mathlib.Topology.MetricSpace.Defs
MetricSpace.replaceBornology_eq : ∀ {α : Type u_3} [m : MetricSpace α] [B : Bornology α]
  (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s), m.replaceBornology H = m
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stmts₁ (Turing.TM2.Stmt.pop k a q) = insert (Turing.TM2.Stmt.pop k a q) (Turing.TM2.stmts₁ q)
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.filterMapₘ : {α : Type u} →
  {β : α → Type v} →
    {δ : α → Type w} → Std.DHashMap.Internal.Raw₀ α β → ((a : α) → β a → Option (δ a)) → Std.DHashMap.Internal.Raw₀ α δ
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the right unitor `ρ_ f`.  -/
Mathlib.Tactic.BicategoryLike.StructuralAtom.rightUnitor : Lean.Expr → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.StructuralAtom
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasProductsOfShape_of_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : Type v₂)
  [CategoryTheory.Limits.HasCoproductsOfShape X Cᵒᵖ], CategoryTheory.Limits.HasProductsOfShape X C
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.sup_le : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (K₁ K₂ : TopologicalSpace.Compacts G),
  μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_eq_self : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] (A : Matrix m n α) (i : n),
  (A.updateCol i fun j => A j i) = A
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.hasIntPow : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [DivInvMonoid β] → Pow (MeasureTheory.SimpleFunc α β) ℤ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpOptions.toWorkDoneProgressOptions : Lean.Lsp.SignatureHelpOptions → Lean.Lsp.WorkDoneProgressOptions
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaCurry_add : ∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι]
  [inst_1 : (i : ι) → (j : α i) → AddZeroClass (δ i j)] (f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd),
  (f + g).sigmaCurry = f.sigmaCurry + g.sigmaCurry
-- Mathlib.Data.Matrix.Composition
Matrix.comp_symm_single : ∀ {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} [inst : DecidableEq I]
  [inst_1 : DecidableEq J] [inst_2 : DecidableEq K] [inst_3 : DecidableEq L] [inst_4 : Zero R] (ii : I × K) (jj : J × L)
  (r : R), (Matrix.comp I J K L R).symm (Matrix.single ii jj r) = Matrix.single ii.1 jj.1 (Matrix.single ii.2 jj.2 r)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.instCharacteristicUpperCentralSeriesStep : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [inst_1 : N.Normal] [N.Characteristic],
  N.upperCentralSeriesStep.Characteristic
-- Init.Data.List.Nat.Sublist
List.infix_iff_getElem? : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁ <:+: l₂ ↔ ∃ k, l₁.length + k ≤ l₂.length ∧ ∀ (i : ℕ) (h : i < l₁.length), l₂[i + k]? = some l₁[i]
-- Mathlib.Computability.StateTransition
StateTransition.tr_reaches₁ : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop},
  StateTransition.Respects f₁ f₂ tr →
    ∀ {a₁ : σ₁} {a₂ : σ₂},
      tr a₁ a₂ → ∀ {b₁ : σ₁}, StateTransition.Reaches₁ f₁ a₁ b₁ → ∃ b₂, tr b₁ b₂ ∧ StateTransition.Reaches₁ f₂ a₂ b₂
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsUniversal.not_isIsolated : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [Nontrivial V], G.IsUniversal v → ∀ (w : V), ¬G.IsIsolated w
-- Mathlib.Topology.Category.CompHaus.Limits
/-- A one-element space is terminal in `CompHaus`  -/
CompHaus.isTerminalPUnit : CategoryTheory.Limits.IsTerminal (CompHaus.of PUnit.{u + 1})
-- Init.Data.Int.Linear
/-- Returns the ceiling-compatible remainder of the division `a / b`.
This function ensures that the remainder is consistent with `cdiv`, meaning:
```
a = b * cdiv a b + cmod a b
```
See theorem `cdiv_add_cmod`. We also have
```
-b < cmod a b ≤ 0
```
 -/
Int.Internal.Linear.cmod : ℤ → ℤ → ℤ
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- If the image under the norm is zero, then the argument is zero.  -/
NonarchAddGroupNormClass.eq_zero_of_map_eq_zero : ∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : AddGroup α} {inst_1 : FunLike F α ℝ}
  [self : NonarchAddGroupNormClass F α] (f : F) {a : α}, f a = 0 → a = 0
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.constantsToVars.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (a : α),
  (FirstOrder.Language.var a).constantsToVars = FirstOrder.Language.var (Sum.inr a)
-- Mathlib.Algebra.Algebra.Epi
/-- See also `Algebra.isEpi_iff_surjective_algebraMap_of_finite`.  -/
Algebra.isEpi_of_surjective_algebraMap : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Surjective ⇑(algebraMap R A) → Algebra.IsEpi R A
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.map_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U : CategoryTheory.Under Y},
  ((CategoryTheory.Under.map f).obj U).hom = CategoryTheory.CategoryStruct.comp f U.hom
-- Std.Http.Data.URI.Basic
Std.Http.URI.Port.value.sizeOf_spec : ∀ (port : UInt16), sizeOf (Std.Http.URI.Port.value port) = 1 + sizeOf port
-- Aesop.Stats.Basic
Aesop.RuleStats.instToString : ToString Aesop.RuleStats
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.iff_comp_neg : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {f : ℝ → E},
  autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.iff_comp_neg._auto_1 →
    (IntervalIntegrable f MeasureTheory.volume a b ↔
      IntervalIntegrable (fun x => f (-x)) MeasureTheory.volume (-a) (-b))
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
/-- If `R : InjectiveResolution X`, then `R.cochainComplex.X n` (with `n : ℕ`)
is isomorphic to `R.cocomplex.X k` (with `k : ℕ`) when `k = n`.  -/
CategoryTheory.InjectiveResolution.cochainComplexXIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {X : C} →
          (R : CategoryTheory.InjectiveResolution X) →
            (n : ℤ) → (k : ℕ) → ↑k = n → (R.cochainComplex.X n ≅ R.cocomplex.X k)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.decl.injEq : ∀ (declName : Lean.Name) (post inv : Bool) (declName_1 : Lean.Name) (post_1 inv_1 : Bool),
  (Lean.Meta.Origin.decl declName post inv = Lean.Meta.Origin.decl declName_1 post_1 inv_1) =
    (declName = declName_1 ∧ post = post_1 ∧ inv = inv_1)
-- Batteries.Data.BitVec.Lemmas
BitVec.toNat_ofFnLEAux : ∀ {n : ℕ} (m : ℕ) (f : Fin n → Bool), (BitVec.ofFnLEAux m f).toNat = Nat.ofBits f % 2 ^ m
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete and then runs the `IO` action `f` on its result.
This new task has priority `prio`.

This is a version of `IO.mapTask` that ignores the result value.

Running the resulting `IO` action causes the task to be started eagerly. Unlike pure tasks created
by `Task.spawn`, tasks created by this function will run even if the last reference to the task is
dropped. The act should explicitly check for cancellation via `IO.checkCanceled` if it should be
terminated or otherwise react to the last reference being dropped.
 -/
IO.chainTask : {α : Type u_1} → Task α → (α → IO Unit) → optParam Task.Priority Task.Priority.default → optParam Bool false → IO Unit
-- Lean.Meta.Sym.Pattern
/-- Substitutes uvars in `u` with their assignments, and then normalize.  -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.substAssignedUVarsAndNormalize : Lean.Level → Lean.Meta.Sym.UnifyM✝ Lean.Level
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).getKey k h' = t.getKey k ⋯
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.id_obj : ∀ (V : Type u_1) [inst : CategoryTheory.ReflQuiver V] (X : V), (𝟭rq V).obj X = X
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- If `L` is a finite extension of `K = Frac(A)`,
then `L` has a basis over `A` consisting of integral elements.  -/
FiniteDimensional.exists_is_basis_integral : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  (L : Type u_3) [inst_4 : Field L] [inst_5 : Algebra K L] [inst_6 : Algebra A L] [IsScalarTower A K L]
  [FiniteDimensional K L] [IsDomain A], ∃ s b, ∀ (x : ↥s), IsIntegral A (b x)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The "inert" morphism associated to a subinterval `j ≤ i ≤ j + l` of `Fin (n + 1)`.  -/
SimplexCategory.subinterval : {n : ℕ} → (j l : ℕ) → j + l ≤ n → ({ len := l } ⟶ { len := n })
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instIsStableUnderShiftExtensionProductInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] [Q.IsStableUnderShift ℤ],
  (P.extensionProduct Q).IsStableUnderShift ℤ
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.image_mem_nhdsWithin : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ {x : X} {s : Set X}, s ∈ nhds x → f '' s ∈ nhdsWithin (f x) (Set.range f)
-- Mathlib.RingTheory.Henselian
HenselianRing.is_henselian : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} [self : HenselianRing R I] (f : Polynomial R),
  f.Monic →
    ∀ (a₀ : R),
      Polynomial.eval a₀ f ∈ I →
        IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f))) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.HoverInfo : Type
-- Mathlib.Logic.Function.Conjugate
/-- Any function semiconjugates the identity function to the identity function.  -/
Function.Semiconj.id_right : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Semiconj f id id
-- Init.NotationExtra
«termΣ_,_» : Lean.ParserDescr
-- Batteries.Data.Char.Basic
/-- Returns `true` if `p` returns true for every `Char`.  -/
Char.all : (Char → Bool) → Bool
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.whiskerRight : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f g : a ⟶ b) →
        (h : b ⟶ c) →
          [CategoryTheory.BicategoricalCoherence f g] →
            CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f h)
              (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.map_centralizer_le_centralizer_image : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (s : Set G) (f : G →+ G'),
  AddSubgroup.map f (AddSubgroup.centralizer s) ≤ AddSubgroup.centralizer (⇑f '' s)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.of_subsingleton_cod : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [Subsingleton α], Summable f L
-- Mathlib.Data.Finsupp.SMul
/-- A version of `Finsupp.comapDomain_smul` that's easier to use.  -/
Finsupp.comapDomain_smul_of_injective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_6} [inst : Zero M] [inst_1 : SMulZeroClass R M] {f : α → β}
  (hf : Function.Injective f) (r : R) (v : β →₀ M), Finsupp.comapDomain f (r • v) ⋯ = r • Finsupp.comapDomain f v ⋯
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph embedding induces a graph isomorphism between its domain and its range  -/
SimpleGraph.Embedding.isoInduceRange : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} → {G' : SimpleGraph W} → (f : G ↪g G') → G ≃g SimpleGraph.induce (Set.range ⇑f) G'
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂IdIso_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} (α : (CategoryTheory.Functor.id C).comp S ⟶ S.comp (CategoryTheory.Functor.id D))
  (T : D) (β : (CategoryTheory.Functor.id D).obj T ⟶ T)
  (hα :
    autoParam (α = CategoryTheory.CategoryStruct.comp S.leftUnitor.hom S.rightUnitor.inv)
      CategoryTheory.CostructuredArrow.map₂IdIso._auto_1)
  (hβ :
    autoParam (β = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj T))
      CategoryTheory.CostructuredArrow.map₂IdIso._auto_3)
  (X : CategoryTheory.CostructuredArrow S T),
  ((CategoryTheory.CostructuredArrow.map₂IdIso α T β hα hβ).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Data.List.Lattice
List.forall_mem_of_forall_mem_union_left : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Prop} [inst : DecidableEq α], (∀ x ∈ l₁ ∪ l₂, p x) → ∀ x ∈ l₁, p x
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNewUnit.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (toInsert : List α) → (Unit → motive []) → ((hd : α) → (tl : List α) → motive (hd :: tl)) → motive toInsert
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.coe_inf : ∀ (μ ν : YoungDiagram), ↑(μ ⊓ ν) = ↑μ ∩ ↑ν
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.tendsto_finsetProd_atTop : ∀ {ι : Type u_1} {ι' : Type u_2}, Filter.Tendsto (fun p => p.1 ×ˢ p.2) Filter.atTop Filter.atTop
-- Lean.Data.NameMap.Basic
Lean.NameSet.ofList : List Lean.Name → Lean.NameSet
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
/-- The image of `g * X - 1` in `I/I²` if `I` is the kernel of the canonical presentation
of the localization of `S` away from `g`.  -/
Algebra.Generators.cMulXSubOneCotangent : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (r : R) → [inst_3 : IsLocalization.Away r S] → (Algebra.Generators.localizationAway S r).toExtension.Cotangent
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.instSMulHom : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → SMul R (S₁ ⟶ S₂)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C))
  (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)) (j : J),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit F U).hom
      (CategoryTheory.Limits.limit.π (AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U) (Opposite.op j)) =
    (CategoryTheory.Limits.colimit.ι F j).c.app (Opposite.op U)
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- If `η_A` is a split monomorphism, then `A` is in the reflective subcategory.  -/
CategoryTheory.mem_essImage_of_unit_isSplitMono : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] {A : C}
  [CategoryTheory.IsSplitMono ((CategoryTheory.reflectorAdjunction i).unit.app A)], i.essImage A
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_findSomeM? : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → m (Option β)) (xs : Array α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.findSomeM? (f x) xs
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_ofList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.TreeMap.Raw.ofList l cmp).isEmpty = l.isEmpty
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.fiber_obj_obj : ∀ (R : Type u) [inst : CommRing R] (Ω : Type w) [inst_1 : Field Ω] [inst_2 : Algebra R Ω]
  (S : (CommAlgCat.FiniteEtale R)ᵒᵖ), ((CommAlgCat.FiniteEtale.fiber R Ω).obj S).obj = (↑(Opposite.unop S).obj →ₐ[R] Ω)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
  (γ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₁ h₂), (γ.add γ').φQ = γ.φQ + γ'.φQ
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- The valuation subring of a valued field is open.  -/
Valued.isOpen_valuationSubring : ∀ {Γ₀ : Type v} [inst : LinearOrderedCommGroupWithZero Γ₀] (K : Type u) [inst_1 : Field K] [hv : Valued K Γ₀],
  IsOpen ↑Valued.v.valuationSubring
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [inst_2 : 𝒰.HasPullbacks]
  (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T)
  (hf :
    ∀ (i j : 𝒰.I₀),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j))
  (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphisms f hf) = f i
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Liff.eq_1 : ∀ (α : Type u) {σ1 : Type v} {σ2 : Type w} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2),
  Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 =
    ∀ (a : α → Bool),
      Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f1 ↔ Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f2
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_K : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_3),
  (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).K = X.cycles f₁ f₂ n₁
-- Mathlib.Topology.MetricSpace.IsometricSMul
Pi.isIsometricVAdd'' : ∀ {ι : Type u_3} {M : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → Add (M i)]
  [inst_2 : (i : ι) → PseudoEMetricSpace (M i)] [∀ (i : ι), IsIsometricVAdd (M i)ᵃᵒᵖ (M i)],
  IsIsometricVAdd ((i : ι) → M i)ᵃᵒᵖ ((i : ι) → M i)
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.insertArray : Lean.NameSet → Array Lean.Name → Lean.NameSet
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryToUnit_pullback_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
  {Y Z : CategoryTheory.Over (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)} (g : Y ⟶ Z),
  (CategoryTheory.ChosenPullbacksAlong.pullback f).map g =
    CategoryTheory.Over.homMk (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Over.Hom.left g) X) ⋯
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_comp : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} {Z : Type w} [inst_6 : AddCommGroup Z] [inst_7 : Module k Z] {τ : Representation k G Z}
  (f : ρ.IntertwiningMap σ) (g : σ.IntertwiningMap τ),
  Rep.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (Rep.ofHom f) (Rep.ofHom g)
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- Construct an `IsLimit` structure of kernels given `Function.Exact`.  -/
ModuleCat.isLimitKernelFork : {R : Type u} →
  [inst : Ring R] →
    {M N P : ModuleCat R} →
      (f : M ⟶ N) →
        (g : N ⟶ P) →
          (H : Function.Exact ⇑(ModuleCat.Hom.hom f) ⇑(ModuleCat.Hom.hom g)) →
            Function.Injective ⇑(ModuleCat.Hom.hom f) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f ⋯)
-- Batteries.Lean.NameMapAttribute
/-- The name of the attribute  -/
Lean.NameMapAttributeImpl.name : {α : Type} → Lean.NameMapAttributeImpl α → Lean.Name
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
Lean.Meta.RefinedDiscrTree.MatchResult.mk.inj : ∀ {α : Type} {elts elts_1 : Std.TreeMap ℕ (Array (Array α)) compare},
  { elts := elts } = { elts := elts_1 } → elts = elts_1
-- Mathlib.Analysis.PSeries
/-- Cauchy condensation test for eventually antitone and nonnegative series of real numbers.  -/
summable_condensed_iff_of_eventually_nonneg : ∀ {f : ℕ → ℝ},
  0 ≤ᶠ[Filter.atTop] f →
    (∀ᶠ (k : ℕ) in Filter.atTop, f (k + 1) ≤ f k) → ((Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f)
-- Mathlib.CategoryTheory.RegularCategory.Basic
/-- In a regular category, every extremal epimorphism is a regular epimorphism.  -/
CategoryTheory.Regular.regularEpiOfExtremalEpi : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Regular C] →
      {X Y : C} → (f : X ⟶ Y) → [h : CategoryTheory.ExtremalEpi f] → CategoryTheory.RegularEpi f