mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R},
  ∑ j, w₁ j = 1 →
    ∑ j, w₂ j = 1 →
      ∀ {i : Fin (n + 1)},
        SignType.sign (w₁ i) = SignType.sign (w₂ i) →
          w₁ i ≠ 0 →
            (affineSpan R (Set.range (s.faceOpposite i).points)).SSameSide
              ((Finset.affineCombination R Finset.univ s.points) w₁)
              ((Finset.affineCombination R Finset.univ s.points) w₂)
-- Mathlib.Logic.Function.Basic
Function.update_idem : ∀ {α : Sort u_2} [inst : DecidableEq α] {β : α → Sort u_1} {a : α} (v w : β a) (f : (a : α) → β a),
  Function.update (Function.update f a v) a w = Function.update f a w
-- Mathlib.CategoryTheory.Monad.Basic
/-- The forgetful functor from the category of monads to the category of endofunctors.
 -/
CategoryTheory.monadToFunctor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor (CategoryTheory.Monad C) (CategoryTheory.Functor C C)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.mono_homologyMap_of_mono_opcyclesMap' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.Mono (CategoryTheory.ShortComplex.opcyclesMap φ) →
    CategoryTheory.Mono (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Data.ZMod.Basic
ZMod.val_mul_of_lt : ∀ {n : ℕ} {a b : ZMod n}, a.val * b.val < n → (a * b).val = a.val * b.val
-- Mathlib.Data.Finset.Basic
Finset.erase_ssubset : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∈ s → s.erase a ⊂ s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.y_mk : ∀ {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1), (Pell.Solution₁.mk x y prop).y = y
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharThreeNF_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.IsCharThreeNF
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheorems.getKindsFor : Lean.Meta.Grind.EMatchTheorems → Lean.Meta.Grind.Origin → List Lean.Meta.Grind.EMatchTheoremKind
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_uInt32ToBitVec : ∀ (n : UInt32), { toBitVec := BitVec.setWidth 16 n.toBitVec } = n.toUInt16
-- Mathlib.Topology.Order.Basic
/-- The set of points which are isolated on the left is countable when the space is
second-countable.  -/
countable_setOfPred_covBy_left : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α],
  {x | ∃ y, y ⋖ x}.Countable
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.mem_map_iff_mem : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N},
  Function.Injective ⇑f → ∀ {K : Subgroup G} {x : G}, f x ∈ Subgroup.map f K ↔ x ∈ K