mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Cycle
/-- Given a `s : Cycle α` such that `Nodup s`, retrieve the previous element before `x ∈ s`.  -/
Cycle.prev : {α : Type u_1} → [DecidableEq α] → (s : Cycle α) → s.Nodup → (x : α) → x ∈ s → α
-- Lean.Parser.Types
Lean.Parser.ParserCacheEntry.mk.inj : ∀ {stx : Lean.Syntax} {lhsPrec : ℕ} {newPos : String.Pos.Raw} {errorMsg : Option Lean.Parser.Error}
  {stx_1 : Lean.Syntax} {lhsPrec_1 : ℕ} {newPos_1 : String.Pos.Raw} {errorMsg_1 : Option Lean.Parser.Error},
  { stx := stx, lhsPrec := lhsPrec, newPos := newPos, errorMsg := errorMsg } =
      { stx := stx_1, lhsPrec := lhsPrec_1, newPos := newPos_1, errorMsg := errorMsg_1 } →
    stx = stx_1 ∧ lhsPrec = lhsPrec_1 ∧ newPos = newPos_1 ∧ errorMsg = errorMsg_1
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_transpose : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β),
  Matrix.kroneckerMap f A.transpose B.transpose = (Matrix.kroneckerMap f A B).transpose
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_inter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, t ∈ nhds x → (ContDiffWithinAt 𝕜 n f (s ∩ t) x ↔ ContDiffWithinAt 𝕜 n f s x)
-- Mathlib.Data.Finmap
Finmap.toFinmap_nil : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α], [].toFinmap = ∅
-- Mathlib.Analysis.BoxIntegral.Basic
/-- If `ε > 0`, then `BoxIntegral.Integrable.convergenceR` is a function `r : ℝ≥0 → ℝⁿ → (0, ∞)`
such that for every `c : ℝ≥0`, for every tagged partition `π` subordinate to `r` (and satisfying
additional distortion estimates if `BoxIntegral.IntegrationParams.bDistortion l = true`), the
corresponding integral sum is `ε`-close to the integral.

If `BoxIntegral.IntegrationParams.bRiemann = true`, then `r c x` does not depend on `x`. If
`ε ≤ 0`, then we use `r c x = 1`.  -/
BoxIntegral.Integrable.convergenceR : {ι : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {I : BoxIntegral.Box ι} →
                [inst_4 : Fintype ι] →
                  {l : BoxIntegral.IntegrationParams} →
                    {f : (ι → ℝ) → E} →
                      {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} →
                        BoxIntegral.Integrable I l f vol → ℝ → NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.rightUnitor_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor F).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom
-- Init.Data.Array.Zip
/-- See also `getElem?_zipWith'` for a variant
using `Option.map` and `Option.bind` rather than a `match`.
 -/
Array.getElem?_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : Array α} {bs : Array β} {f : α → β → γ} {i : ℕ},
  (Array.zipWith f as bs)[i]? =
    match as[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none
-- Std.Tactic.BVDecide.Syntax
/-- Set SAT solver options to improve proof search.
 -/
Lean.Elab.Tactic.BVDecide.SolverMode.proof : Lean.Elab.Tactic.BVDecide.SolverMode
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKey! k' = k
-- Mathlib.Algebra.Lie.Basic
LieEquiv.symm_apply_eq : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R⁆ L₂) {x : L₂} {y : L₁}, e.symm x = y ↔ x = e y
-- Lean.Util.LeanOptions
Lean.instValueLeanOptionValue : Lean.KVMap.Value Lean.LeanOptionValue
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Icc_left : ∀ {α : Type v} [inst : Preorder α] (a : α), ⋃ b, Set.Icc b a = Set.Iic a
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Proof of type equality as a function  -/
MvPFunctor.castLastB : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {a a' : P.A} → a = a' → P.last.B a → P.last.B a'
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_mul_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [i : MulRightMono α] {b c : α}, b ≤ c → ∀ (a : α), b * a ≤ c * a
-- Mathlib.Order.Preorder.Chain
IsChain.image_relEmbedding_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} {φ : r ↪r r'},
  IsChain r' (⇑φ '' s) ↔ IsChain r s
-- Mathlib.Data.Finsupp.SMul
Finsupp.support_smul_eq : ∀ {α : Type u_1} {M : Type u_3} {R : Type u_6} [inst : Semiring R] [IsDomain R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] {b : R}, b ≠ 0 → ∀ {g : α →₀ M}, (b • g).support = g.support