mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SupIndep
iSupIndep_fin_three : ∀ {α : Type u_5} [inst : CompleteLattice α] {f : Fin 3 → α},
  iSupIndep f ↔ Disjoint (f 0) (f 1 ⊔ f 2) ∧ Disjoint (f 1) (f 2 ⊔ f 0) ∧ Disjoint (f 2) (f 0 ⊔ f 1)
-- Batteries.Data.List.Lemmas
List.diff.eq_def : ∀ {α : Type u_1} [inst : BEq α] (x x_1 : List α),
  x.diff x_1 =
    match x, x_1 with
    | l, [] => l
    | l₁, a :: l₂ => if List.elem a l₁ = true then (l₁.erase a).diff l₂ else l₁.diff l₂
-- Mathlib.NumberTheory.ADEInequality
/-- `E8 := {2,3,5}` is a `Multiset ℕ+`
that is a solution to the inequality
`(p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1`.

This solution is related to the Dynkin diagrams $E_8$.  -/
ADEInequality.E8 : Multiset ℕ+
-- Mathlib.Order.Antisymmetrization
/-- The partial order derived from a preorder by making pairwise comparable elements equal. This is
the quotient by `fun a b => a ≤ b ∧ b ≤ a`.  -/
Antisymmetrization : (α : Type u_1) → (r : α → α → Prop) → [IsPreorder α r] → Type u_1
-- Mathlib.Data.Fin.Basic
Fin.le_val_last : ∀ {n : ℕ} (i : Fin (n + 1)), i ≤ ↑n
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.card_toZFSet : ∀ (o : Ordinal.{u_1}), o.toZFSet.card = o.card
-- Mathlib.GroupTheory.Complement
/-- `H` and `K` are complements if `(*) : H × K → G` is a bijection  -/
Subgroup.IsComplement' : {G : Type u_1} → [inst : Group G] → Subgroup G → Subgroup G → Prop
-- Lean.Parser.Basic
/-- Parses a raw string literal assuming `isRawStrLitStart` has returned true.
The `startPos` is the start of the raw string (at the `r`).
The parser state is assumed to be immediately after the `r`.
 -/
Lean.Parser.rawStrLitFnAux : String.Pos.Raw → Lean.Parser.ParserFn
-- Init.Core
toBoolUsing_eq_true : ∀ {p : Prop} (d : Decidable p), p → toBoolUsing d = true
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- For any two charts `e`, `e'` around a point `x` in a C¹ manifold, `e` maps `x` to the interior
of the model space iff `e'` does. - in other words, the notion of interior points does not
depend on any choice of charts.  -/
ModelWithCorners.mem_interior_range_iff_of_mem_atlas : ∀ {𝕜 : 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] {n : WithTop ℕ∞} [IsManifold I n M]
  {e e' : OpenPartialHomeomorph M H} {x : M},
  n ≠ 0 →
    e ∈ atlas H M →
      e' ∈ atlas H M →
        x ∈ e.source →
          x ∈ e'.source →
            (↑(e.extend I) x ∈ interior (e.extend I).target ↔ ↑(e'.extend I) x ∈ interior (e'.extend I).target)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.getVert_injOn' : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → Set.InjOn p.getVert {i | i ≤ p.length - 1}
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.eq_1 : ∀ {σ : String.Slice → Type} [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  {s : String.Slice} (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (motive : searcher.Step → Sort u_1)
  (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s)) (startPos endPos : s.Pos)
  (hps :
    searcher.IsPlausibleStep (Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos)))
  (h_1 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos_1 endPos_1 : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1))) →
          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩ →
            motive
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩)
  (h_2 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos_1 endPos_1 : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1))) →
          ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩ →
            motive
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩)
  (h_3 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (hps_1 : searcher.IsPlausibleStep (Std.IterStep.skip searcher'_1)) →
        ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =
            ⟨Std.IterStep.skip searcher'_1, hps_1⟩ →
          motive ⟨Std.IterStep.skip searcher'_1, hps_1⟩)
  (h_4 :
    (property : searcher.IsPlausibleStep Std.IterStep.done) →
      ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ =
          ⟨Std.IterStep.done, property⟩ →
        motive ⟨Std.IterStep.done, property⟩),
  (match h : ⟨Std.IterStep.yield searcher' (String.Slice.Pattern.SearchStep.matched startPos endPos), hps⟩ with
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos_1 endPos_1), hps_1⟩ =>
      h_1 searcher'_1 startPos_1 endPos_1 hps_1 h
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos_1 endPos_1), hps_1⟩ =>
      h_2 searcher'_1 startPos_1 endPos_1 hps_1 h
    | ⟨Std.IterStep.skip searcher'_1, hps_1⟩ => h_3 searcher'_1 hps_1 h
    | ⟨Std.IterStep.done, property⟩ => h_4 property h) =
    h_1 searcher' startPos endPos hps ⋯
-- Std.Data.HashMap.Lemmas
Std.HashMap.fold_eq_foldl_toArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {f : δ → α → β → δ}
  {init : δ}, Std.HashMap.fold f init m = Array.foldl (fun a b => f a b.1 b.2) init m.toArray
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.throwInvalidExplicitUniversesForLocal : {α : Type} → Lean.Expr → Lean.Elab.TermElabM α
-- Init.Data.Nat.Lemmas
Nat.instIdempotentOpMin : Std.IdempotentOp min
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.awayMap_fromZeroRingHom : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e : ι} {f g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g) (a : ↥(𝒜 0)),
  (HomogeneousLocalization.awayMap 𝒜 hg hx) ((HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)) a) =
    (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers x)) a
-- Init.Data.String.Search
/-- Splits a string at each subslice that matches the pattern `pat`.

The subslices that matched the pattern are not included in any of the resulting subslices. If
multiple subslices in a row match the pattern, the resulting list will contain empty strings.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`

* `("coffee tea water".split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`

* `("coffee tea water".split " tea ").toList == ["coffee".toSlice, "water".toSlice]`

* `("ababababa".split "aba").toList == ["".toSlice, "b".toSlice, "ba".toSlice]`

* `("baaab".split "aa").toList == ["b".toSlice, "ab".toSlice]`
 -/
String.split : {ρ : Type} →
  {σ : String.Slice → Type} →
    [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      (s : String) → (pat : ρ) → [inst : String.Slice.Pattern.ToForwardSearcher pat σ] → Std.Iter String.Slice
-- Lean.Server.Utils
/-- Constructs a `$/lean/fileProgress` notification.  -/
Lean.Server.mkFileProgressNotification : Lean.Server.DocumentMeta →
  Array Lean.Lsp.LeanFileProgressProcessingInfo → Lean.JsonRpc.Notification Lean.Lsp.LeanFileProgressParams
-- Mathlib.CategoryTheory.ComposableArrows.Basic
Fin.natAddLEFunctor.congr_simp : ∀ {n k k_1 : ℕ} (e_k : k = k_1) {l : ℕ} (h : k + l ≤ n), Fin.natAddLEFunctor h = Fin.natAddLEFunctor ⋯
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.toNonUnitalSubsemiring_top : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], ⊤.toNonUnitalSubsemiring = ⊤