mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.not_facet_iff_subface : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s : Finset E},
  s ∈ K.faces → (s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  HasFDerivAt (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis)
    (NumberField.mixedEmbedding.fundamentalCone.fderiv_expMapBasis K x) x
-- Mathlib.Data.Sum.Order
Sum.instTrichotomousLex_mathlib : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [Std.Trichotomous r] [Std.Trichotomous s],
  Std.Trichotomous (Sum.Lex r s)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Adjunction.mapAddGrp_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal],
  a.mapAddGrp.unit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapAddGrpIdIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapAddGrpNatTrans a.unit)
        CategoryTheory.Functor.mapAddGrpCompIso.hom)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.connectedComponentMk_supp_subset_supp : ∀ {V : Type u} {G G' : SimpleGraph V} {v : V},
  G ≤ G' → ∀ (c' : G'.ConnectedComponent), v ∈ c'.supp → (G.connectedComponentMk v).supp ⊆ c'.supp
-- Mathlib.Data.QPF.Univariate.Basic
QPF.abs : {F : Type u → Type v} → [self : QPF F] → {α : Type u} → ↑(QPF.P F) α → F α
-- Mathlib.Algebra.Group.Ext
AddCancelMonoid.toAddRightCancelMonoid_injective : ∀ {M : Type u}, Function.Injective (@AddCancelMonoid.toAddRightCancelMonoid M)
-- Mathlib.Algebra.Group.Defs
NPow.mk : {M : Type u} → (ℕ → M → M) → NPow M
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₂.getKey k ⋯
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `(S, F ⋙ G) ⥤ (S, G)`.  -/
CategoryTheory.StructuredArrow.pre : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {B : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} B] →
            (S : D) →
              (F : CategoryTheory.Functor B C) →
                (G : CategoryTheory.Functor C D) →
                  CategoryTheory.Functor (CategoryTheory.StructuredArrow S (F.comp G))
                    (CategoryTheory.StructuredArrow S G)
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_flip : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N),
  Submodule.map₂ f.flip q p = Submodule.map₂ f p q
-- Mathlib.Probability.Kernel.Deterministic
/-- in a standard Borel space, a deterministic Markov kernel is a Dirac kernel of one measurable
function.  -/
ProbabilityTheory.Kernel.IsDeterministic.exists_eq_deterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [StandardBorelSpace β]
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsDeterministic κ],
  ∃ f, ∃ (hf : Measurable f), κ = ProbabilityTheory.Kernel.deterministic f hf
-- Mathlib.Order.Interval.Set.OrdConnected
Set.OrdConnected.dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.OrdConnected → (⇑OrderDual.ofDual ⁻¹' s).OrdConnected
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.one_eventuallyLE_mul_atTop : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M}, 1 ≤ᶠ[l] f → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.Entry.token.injEq : ∀ (val val_1 : Lean.Parser.Token),
  (Lean.Parser.ParserExtension.Entry.token val = Lean.Parser.ParserExtension.Entry.token val_1) = (val = val_1)
-- Lean.Compiler.LCNF.Types
/-- Whether the type is a pointer for sure.
 -/
Lean.Compiler.LCNF.ImpureType.Lean.Expr.isDefiniteRef : Lean.Expr → Bool
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.N_one : ∀ {G : Type u} [inst : Group G] (B : GroupFilterBasis G), B.N 1 = B.filter
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.coinduced.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [inst : Group β] (f : α → β),
  GroupTopology.coinduced f = sInf {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- `gramSchmidt` produces a triangular matrix of vectors when given a basis.  -/
InnerProductSpace.gramSchmidt_triangular : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {i j : ι},
  i < j → ∀ (b : Module.Basis ι 𝕜 E), (b.repr (InnerProductSpace.gramSchmidt 𝕜 (⇑b) i)) j = 0
-- Init.Data.String.Search
String.foldrAux : {α : Type u} → (Char → α → α) → α → String → String.Pos.Raw → String.Pos.Raw → α
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.comp_hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' : 𝕜'} {t : Set 𝕜'},
  HasDerivWithinAt h₂ h₂' t (h x) →
    HasDerivAt h h' x → (∀ᶠ (x' : 𝕜) in nhds x, h x' ∈ t) → HasDerivAt (h₂ ∘ h) (h₂' * h') x
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A wide coequalizer morphism is an epimorphism  -/
CategoryTheory.Limits.wideCoequalizer.π_epi : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J],
  CategoryTheory.Epi (CategoryTheory.Limits.wideCoequalizer.π f)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_of_mem_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  s ∈ nhds x → (HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x)
-- Init.Data.Vector.MapIdx
Vector.mapIdx_eq_mapIdx_iff : ∀ {α : Type u_1} {n : ℕ} {α_1 : Type u_2} {f g : ℕ → α → α_1} {xs : Vector α n},
  Vector.mapIdx f xs = Vector.mapIdx g xs ↔ ∀ (i : ℕ) (h : i < n), f i xs[i] = g i xs[i]