mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_eq : ∀ {Ω : Type u_1} {β : Type u_2} {u : ℕ → Ω → β} {τ : Ω → ℕ∞} [inst : AddCommMonoid β] {N : ℕ},
  (∀ (ω : Ω), τ ω ≤ ↑N) →
    MeasureTheory.stoppedValue u τ = fun x => (∑ i ∈ Finset.range (N + 1), {ω | τ ω = ↑i}.indicator (u i)) x
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.forget_map : ∀ {X Y : GrpWithZero} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget GrpWithZero).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.Matrix.Mul
Matrix.add_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  (A : Matrix m n α) (x y : m → α), Matrix.vecMul (x + y) A = Matrix.vecMul x A + Matrix.vecMul y A
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
toMul_multiset_sum : ∀ {M : Type u_3} [inst : CommMonoid M] (s : Multiset (Additive M)),
  Additive.toMul s.sum = (Multiset.map (⇑Additive.toMul) s).prod
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort'.eq_def : ∀ (s acc : Lean.Grind.AC.Seq),
  s.sort' acc =
    match s with
    | Lean.Grind.AC.Seq.var x => Lean.Grind.AC.Seq.insert x acc
    | Lean.Grind.AC.Seq.cons x s => s.sort' (Lean.Grind.AC.Seq.insert x acc)
-- Mathlib.Combinatorics.Additive.SubsetSum
Finset.subsetSum_mono : ∀ {M : Type u_1} [inst : DecidableEq M] [inst_1 : AddCommMonoid M] {A B : Finset M}, A ⊆ B → A.subsetSum ⊆ B.subsetSum
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_6 : ∀ (cf cg : Nat.Partrec.Code), (cf.comp cg).eval = fun n => cg.eval n >>= cf.eval
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict.comm : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {e : c.Embedding c'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e) (i j : ι),
  CategoryTheory.CategoryStruct.comp (ComplexShape.Embedding.homRestrict.f ψ i) (L.d i j) =
    CategoryTheory.CategoryStruct.comp (K.d (e.f i) (e.f j)) (ComplexShape.Embedding.homRestrict.f ψ j)