mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Chebyshev
/-- `θ x` is the log of the product of the primes up to `x`.  -/
Chebyshev.theta_eq_log_primorial : ∀ (x : ℝ), Chebyshev.theta x = Real.log ↑(primorial ⌊x⌋₊)
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
LaurentPolynomial.counit_C_mul_T : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A) (n : ℤ),
  CoalgebraStruct.counit (LaurentPolynomial.C a * LaurentPolynomial.T n) = CoalgebraStruct.counit a
-- Mathlib.Control.EquivFunctor
EquivFunctor.mk : {f : Type u₀ → Type u₁} →
  (map : {α β : Type u₀} → α ≃ β → f α → f β) →
    autoParam (∀ (α : Type u₀), map (Equiv.refl α) = id) EquivFunctor.map_refl'._autoParam →
      autoParam (∀ {α β γ : Type u₀} (k : α ≃ β) (h : β ≃ γ), map (k.trans h) = map h ∘ map k)
          EquivFunctor.map_trans'._autoParam →
        EquivFunctor f
-- Mathlib.Algebra.Order.Group.Abs
inv_le_of_mabs_le : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, |a|ₘ ≤ b → b⁻¹ ≤ a
-- Std.Time.Time.PlainTime
/-- Creates a `PlainTime` value from a total number of nanoseconds.
 -/
Std.Time.PlainTime.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.PlainTime
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.ringFunc.neg : FirstOrder.ringFunc 1
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.toComon_map_hom : ∀ (R : Type u) [inst : CommRing R] {X Y : CoalgCat R} (f : X ⟶ Y),
  ((CoalgCat.toComon R).map f).hom = ModuleCat.ofHom ↑f.toCoalgHom'
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- The inverse function is approximated linearly on `f '' s` by `f'.symm`.  -/
ApproximatesLinearOn.to_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c)
  (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹),
  ApproximatesLinearOn (↑(hf.toPartialEquiv hc).symm) (↑f'.symm) (f '' s) (‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (t.insertMany l)[k]? =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if cmp a k = Ordering.eq then some b else none)
              l).or
          t[k]?
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The underlying homomorphism of `C`.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.val : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} → A.Hom B → (A.obj ⟶ B.obj)
-- Init.Data.Nat.Basic
Nat.lt_of_sub_eq_succ : ∀ {m n l : ℕ}, m - n = l.succ → n < m
-- Aesop.Rule.Forward
/-- If a `ForwardRulePriority` contains a penalty, extract it.  -/
Aesop.ForwardRulePriority.penalty? : Aesop.ForwardRulePriority → Option ℤ
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_ofNatList : ∀ (l : List ℕ) (h : ∀ p ∈ l, Nat.Prime p), ↑(PrimeMultiset.ofNatList l h).prod = l.prod
-- Mathlib.Order.Filter.Basic
Filter.frequently_true_iff_neBot : ∀ {α : Type u} (f : Filter α), (∃ᶠ (x : α) in f, True) ↔ f.NeBot
-- Mathlib.Tactic.Determinant.Bird.Cert
Mathlib.Tactic.Determinant.CertCache.mk.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {rα : Q(CommRing «$α»)}
  {entryCache : Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)}
  {iterStepEntryCache : Std.HashMap (ℕ × ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)}
  {diagCache entryCache_1 : Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)}
  {iterStepEntryCache_1 : Std.HashMap (ℕ × ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)}
  {diagCache_1 : Std.HashMap (ℕ × ℕ) (Mathlib.Tactic.Determinant.Cert rα)},
  { entryCache := entryCache, iterStepEntryCache := iterStepEntryCache, diagCache := diagCache } =
      { entryCache := entryCache_1, iterStepEntryCache := iterStepEntryCache_1, diagCache := diagCache_1 } →
    entryCache = entryCache_1 ∧ iterStepEntryCache = iterStepEntryCache_1 ∧ diagCache = diagCache_1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMapIso_inv : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A] {X : C}
  (data : F.PreOneHypercoverDenseData X) {P Q : CategoryTheory.Functor C₀ᵒᵖ A} (e : P ≅ Q),
  (data.multicospanMapIso e).inv = data.multicospanMap e.inv
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Std.IterStep.successor.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Data.List.MinMax
List.min_le_of_le' : ∀ {α : Type u_1} [inst : LinearOrder α] {l : List α} {a x : α} (b : α), x ∈ l → x ≤ a → List.foldr min b l ≤ a
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_lt_ofNat_iff : ∀ {a : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], Cardinal.lift.{v, u} a < OfNat.ofNat n ↔ a < OfNat.ofNat n
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
/-- The center of continuous linear maps on a topological vector space
with separating dual is trivial, in other words, it is a central algebra.  -/
Algebra.IsCentral.instContinuousLinearMap : ∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace V] [IsTopologicalRing R] [inst_5 : Module R V] [SeparatingDual R V]
  [inst_7 : IsTopologicalAddGroup V] [ContinuousSMul R V] {S : Type u_3} [inst_9 : CommSemiring S]
  [inst_10 : Module S V] [inst_11 : SMulCommClass R S V] [inst_12 : Algebra S R] [inst_13 : IsScalarTower S R V]
  [inst_14 : ContinuousConstSMul S V] [Algebra.IsCentral S R], Algebra.IsCentral S (V →L[R] V)
-- Mathlib.Algebra.Star.Unitary
Unitary.instCommGroupSubtypeMemSubmonoidUnitary : {R : Type u_1} → [inst : CommMonoid R] → [inst_1 : StarMul R] → CommGroup ↥(unitary R)
-- Mathlib.NumberTheory.Divisors
Nat.card_divisors_le_self : ∀ (n : ℕ), n.divisors.card ≤ n
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.algebraMap_eq_of_integral : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [ifr : IsFractionRing R K] [IsIntegrallyClosed R] {x : K}, IsIntegral R x → ∃ y, (algebraMap R K) y = x
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.numDenom_div : ∀ {K : Type u} [inst : Field K] (p : Polynomial K) {q : Polynomial K},
  q ≠ 0 →
    ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).numDenom =
      (Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q),
        Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the products `W ⨯ X` and `Y ⨯ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and
`g : X ≅ Z` induces an isomorphism `prod.mapIso f g : W ⨯ X ≅ Y ⨯ Z`.  -/
CategoryTheory.Limits.prod.mapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] →
        [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z] → (W ≅ Y) → (X ≅ Z) → (W ⨯ X ≅ Y ⨯ Z)
-- Mathlib.Algebra.Ring.Defs
/-- **Alias** of `right_distrib`. -/
add_mul : ∀ {R : Type v} [inst : Mul R] [inst_1 : Add R] [RightDistribClass R] (a b c : R), (a + b) * c = a * c + b * c
-- Init.Data.List.Perm
List.modifyTailIdx.eq_1 : ∀ {α : Type u} (l : List α) (i : ℕ) (f : List α → List α), l.modifyTailIdx i f = List.modifyTailIdx.go f i l
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.closure_singleton_le_iff_mem : ∀ {M : Type u_1} [inst : Add M] (m : M) (p : AddSubsemigroup M), AddSubsemigroup.closure {m} ≤ p ↔ m ∈ p
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The supremum of a collection of subspaces is equal to the span of the union of the
collection.  -/
Projectivization.Subspace.span_iUnion : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Sort u_3}
  (s : ι → Set (Projectivization K V)),
  Projectivization.Subspace.span (⋃ i, s i) = ⨆ i, Projectivization.Subspace.span (s i)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropWhile_dropWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice}, (s.dropWhile pat).dropWhile pat = s.dropWhile pat
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- **Alias** of `AlgebraicGeometry.tilde.toOpen`.

---

The map from `M` to `Γ(M, U)`. This is a localization map when `U = D(f)`.  -/
ModuleCat.Tilde.toOpen : {R : CommRingCat} →
  (M : ModuleCat ↑R) →
    (U : (AlgebraicGeometry.Spec R).Opens) →
      M ⟶ (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.obj (Opposite.op U)
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
/-- The quadratic version of `Finsupp.apply_linearCombination`.  -/
QuadraticMap.apply_linearCombination : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (Q : QuadraticMap R M N) {g : ι → M} (l : ι →₀ R),
  Q ((Finsupp.linearCombination R g) l) =
    (Finsupp.linearCombination R (⇑Q ∘ g)) (l * l) +
      ∑ p ∈ l.support.sym2 with ¬p.IsDiag, (Sym2.map (⇑l) p).mul • QuadraticMap.polarSym2 (⇑Q) (Sym2.map g p)
-- Mathlib.CategoryTheory.Equivalence
/-- A functor is an equivalence of categories if it is faithful, full and
essentially surjective.  -/
CategoryTheory.Functor.IsEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Std.Time.DateTime
/-- Subtract `Month.Offset` from a `DateTime`, clipping to the last valid day.
 -/
Std.Time.DateTime.subMonthsClip : Std.Time.DateTime → Std.Time.Month.Offset → Std.Time.DateTime
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono' φ h).φQ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).Q
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.abelian_iff_derived_one_eq_bot : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  IsLieAbelian ↥I ↔ LieAlgebra.derivedSeriesOfIdeal R L 1 I = ⊥
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- A functor `F : C ⥤ D` between monoidal categories is lax monoidal if it is
equipped with morphisms `ε : 𝟙_ D ⟶ F.obj (𝟙_ C)` and `μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)`,
satisfying the appropriate coherences.  -/
CategoryTheory.Functor.LaxMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory D] → CategoryTheory.Functor C D → Type (max u₁ v₂)
-- Init.Data.Array.Lemmas
Array.push_ne_self : ∀ {α : Type u_1} {a : α} {xs : Array α}, xs.push a ≠ xs
-- Init.Data.Rat.Basic
/-- Form the quotient `n / d` where `n d : Int`.  -/
Rat.«term_/._» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.sum_le_tsum : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] [L.NeBot] [L.LeAtTop] {f : ι → α}
  (s : Finset ι), (∀ i ∉ s, 0 ≤ f i) → Summable f L → ∑ i ∈ s, f i ≤ ∑'[L] (i : ι), f i
-- Init.Data.Sum.Basic
Sum.instDecidableRelSumLex : {α : Type u_1} →
  {r : α → α → Prop} →
    {α_1 : Type u_2} → {s : α_1 → α_1 → Prop} → [DecidableRel r] → [DecidableRel s] → DecidableRel (Sum.Lex r s)
-- Mathlib.LinearAlgebra.FreeModule.ModN
/-- `ModN G n` denotes the quotient of `G` by multiples of `n`  -/
ModN : (G : Type u_1) → [AddCommGroup G] → ℕ → Type u_1
-- Mathlib.Topology.Separation.Lemmas
CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuum : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T35Space X], Cardinal.mk X < Cardinal.continuum → TotallySeparatedSpace X
-- Batteries.Lean.Except
_private.Batteries.Lean.Except.0.ExceptT.bindCont.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal monomorphism is a morphism which is the kernel of some morphism.  -/
CategoryTheory.NormalMono.Z : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {X Y : C} →
      {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} → (f : X ⟶ Y) → [self : CategoryTheory.NormalMono f] → C
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.emultiplicity_eq_emultiplicity_span`. -/
emultiplicity_eq_emultiplicity_span : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R},
  emultiplicity (Ideal.span {a}) (Ideal.span {b}) = emultiplicity a b
-- Init.Data.Fin.Lemmas
Fin.mk_zero : ∀ {n : ℕ}, ⟨0, ⋯⟩ = 0
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.lift_comp_of : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_4} [inst_1 : Monoid N]
  (fi : (i : ι) → M i →* N) (i : ι), (Monoid.CoprodI.lift fi).comp Monoid.CoprodI.of = fi i
-- Mathlib.Combinatorics.Quiver.Schreier
/-- The monoid acts on the vertices of the Schreier graph.  -/
Quiver.SchreierGraph.instMulAction : (V : Type u_1) →
  {M : Type u_2} →
    [inst : Monoid M] → [inst_1 : MulAction M V] → {S : Type u_3} → (ι : S → M) → MulAction M (Quiver.SchreierGraph V ι)
-- Mathlib.RingTheory.Flat.TorsionFree
/-- Scalar multiplication `m ↦ r • m` by a regular `r` is injective on a flat module.  -/
Module.Flat.isSMulRegular_of_isRegular : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R},
  IsRegular r → ∀ [Module.Flat R M], IsSMulRegular M r
-- Mathlib.Data.DFinsupp.NeLocus
DFinsupp.neLocus_zero_right : ∀ {α : Type u_1} {N : α → Type u_2} [inst : DecidableEq α] [inst_1 : (a : α) → DecidableEq (N a)]
  [inst_2 : (a : α) → Zero (N a)] (f : Π₀ (a : α), N a), f.neLocus 0 = f.support
-- Init.Data.Int.DivMod.Lemmas
Int.emod_lt_of_neg : ∀ (a : ℤ) {b : ℤ}, b < 0 → a % b < -b
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.term.sizeOf_spec : ∀ (i : Lean.Term), sizeOf (Aesop.Frontend.Feature.term i) = 1 + sizeOf i
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
/-- If `f` is a `(n + 1)`-multilinear alternating map, `x` is an element of the domain,
and `v` is an `n`-vector, then the value of `f` at `v` with `x` inserted at the `p`th place
equals `(-1) ^ p` times the value of `f` at `v` with `x` prepended.  -/
AlternatingMap.map_insertNth : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→ₗ[R] N) (p : Fin (n + 1)) (x : M)
  (v : Fin n → M), f (p.insertNth x v) = (-1) ^ ↑p • f (Matrix.vecCons x v)
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.orthogonalProjectionOnto_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E},
  T.IsPositive →
    ∀ (U : Submodule 𝕜 E) [inst_3 : U.HasOrthogonalProjection],
      (U.orthogonalProjectionOnto ∘SL T ∘SL U.subtypeL).IsPositive
-- Init.Data.Array.Basic
/-- Returns the index of the first element equal to `a`, or `none` if no element is equal to `a`.

Examples:
* `#["carrot", "potato", "broccoli"].idxOf? "carrot" = some 0`
* `#["carrot", "potato", "broccoli"].idxOf? "broccoli" = some 2`
* `#["carrot", "potato", "broccoli"].idxOf? "tomato" = none`
* `#["carrot", "potato", "broccoli"].idxOf? "anything else" = none`
 -/
Array.idxOf? : {α : Type u} → [BEq α] → Array α → α → Option ℕ
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.restrict_carrier : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)), ↑(X.restrict h).toPresheafedSpace = U
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_bot : ∀ {V : Type u} {G : SimpleGraph V}, ⊥.spanningCoe = ⊥
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.instMonadCanonRingM : Lean.Meta.Sym.Arith.MonadCanon Lean.Meta.Grind.Arith.CommRing.RingM
-- Mathlib.Order.WithBot
/-- **Alias** of the reverse direction of `WithTop.untop_le_untop_iff`. -/
WithTop.untop_mono : ∀ {α : Type u_1} [inst : LE α] {x y : WithTop α} (hx : x ≠ ⊤) (hy : y ≠ ⊤), y ≤ x → y.untop hy ≤ x.untop hx
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.splitBy.loop.match_1.splitter : {α : Type u_1} →
  (motive : List α → α → List α → List (List α) → Sort u_2) →
    (x : List α) →
      (x_1 : α) →
        (x_2 : List α) →
          (x_3 : List (List α)) →
            ((a : α) → (as : List α) → (b : α) → (r : List α) → (acc : List (List α)) → motive (a :: as) b r acc) →
              ((ag : α) → (r : List α) → (acc : List (List α)) → motive [] ag r acc) → motive x x_1 x_2 x_3
-- Mathlib.Topology.Separation.Regular
closed_nhdsSet_basis : ∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] (u : Set X),
  IsClosed u → (nhdsSet u).HasBasis (fun s => s ∈ nhdsSet u ∧ IsClosed s) id
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.NatTrans.PullbackShift.natIsoComp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  (F : CategoryTheory.Functor C D) {E : Type u_5} [inst_6 : CategoryTheory.Category.{v_3, u_5} E]
  [inst_7 : CategoryTheory.HasShift E B] (G : CategoryTheory.Functor D E),
  CategoryTheory.NatTrans.PullbackShift.natIsoComp φ F G =
    CategoryTheory.Iso.refl (CategoryTheory.PullbackShift.functor φ (F.comp G))
-- Init.Data.SInt.Lemmas
Int32.mod_self : ∀ {a : Int32}, a % a = 0
-- Std.Time.Date.Unit.Day
Std.Time.Day.instLEOrdinal : LE Std.Time.Day.Ordinal
-- Mathlib.MeasureTheory.Measure.Support
/-- The support of a measure equals the set of points whose open neighborhoods
all have positive measure.  -/
MeasureTheory.Measure.support_eq_forall_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  μ.support = {x | ∀ (u : Set X), x ∈ u → IsOpen u → 0 < μ u}
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.le_toPrecoverage_toGrothendieck : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] (J : CategoryTheory.Precoverage C),
  J ≤ J.toGrothendieck.toPrecoverage
-- Mathlib.Data.Num.Lemmas
PosNum.testBit.eq_3 : ∀ (a : PosNum), a.bit0.testBit 0 = false
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanFileProgressProcessingInfo.toJson : Lean.Lsp.LeanFileProgressProcessingInfo → Lean.Json
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
eval₂_minpolyDiv_of_eval₂_eq_zero : ∀ {R : Type u_3} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_1}
  [inst_3 : CommRing T] [IsDomain T] [inst_5 : DecidableEq T] {x : S} {y : T} (σ : S →+* T),
  Polynomial.eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0 →
    Polynomial.eval₂ σ y (minpolyDiv R x) =
      if σ x = y then σ ((Polynomial.aeval x) (Polynomial.derivative (minpoly R x))) else 0
-- Mathlib.Analysis.Calculus.TangentCone.DimOne
/-- **Alias** of the reverse direction of `uniqueDiffWithinAt_iff_accPt`.

---

In one dimension, a point is a point of unique differentiability of a set
iff it is an accumulation point of the set.  -/
AccPt.uniqueDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {s : Set 𝕜} {x : 𝕜},
  AccPt x (Filter.principal s) → UniqueDiffWithinAt 𝕜 s x
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α →₀ γ) (g : β →₀ γ) (x : β),
  (f.sumElim g) (Sum.inr x) = g x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Mathlib.Topology.Hom.Open
ContinuousOpenMapClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : TopologicalSpace α]
  [inst_1 : TopologicalSpace β] [inst_2 : FunLike F α β] [toContinuousMapClass : ContinuousMapClass F α β],
  (∀ (f : F), IsOpenMap ⇑f) → ContinuousOpenMapClass F α β
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- At `0` the Gamma function is undefined; by convention we assign it the value `0`.  -/
Real.Gamma_zero : Real.Gamma 0 = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- A bilinear form is separating left if the quadratic form it is associated with is anisotropic.
 -/
LinearMap.BilinForm.separatingLeft_of_anisotropic : ∀ {R : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, (LinearMap.BilinMap.toQuadraticMap B).Anisotropic → LinearMap.SeparatingLeft B
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.NonlinearRightInverse.right_inv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {f : E →SL[σ] F} (fsymm : f.NonlinearRightInverse)
  (y : F), f (fsymm.toFun y) = y
-- Mathlib.RepresentationTheory.Basic
Representation.ofMulActionSelfAsModuleEquiv_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G]
  (a : (Representation.ofMulAction k G G).asModule),
  Representation.ofMulActionSelfAsModuleEquiv a = (Representation.ofMulAction k G G).asModuleEquiv.toAddEquiv.toFun a
-- Init.Data.String.Defs
String.instInhabitedPos_1 : {s : String.Slice} → Inhabited s.Pos
-- Std.Sat.AIG.CNF
/-- No entry is invalidated.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.IsExtensionBy.extension : ∀ {aig : Std.Sat.AIG ℕ} {cnf1 cnf2 : Std.Sat.CNF ℕ} {cache1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf1}
  {cache2 : Std.Sat.AIG.toCNF.Cache✝ aig cnf2} {new : ℕ} {hnew : new < aig.decls.size},
  Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache1 cache2 new hnew →
    ∀ (idx : ℕ) (hidx : idx < aig.decls.size),
      (Std.Sat.AIG.toCNF.Cache.marks✝ cache1)[idx] = true → (Std.Sat.AIG.toCNF.Cache.marks✝ cache2)[idx] = true