mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Util.CompileInductive
_private.Mathlib.Util.CompileInductive.0.Mathlib.Util.compileStructOnly.go : Lean.InductiveVal → Lean.RecursorVal → Lean.Expr → Lean.MetaM Unit
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_pos_of_pos : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a : α}, 0 < a → 0 < |a|
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.liftK_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) {A : C} (k : A ⟶ S.X₂)
  (hk : CategoryTheory.CategoryStruct.comp k S.g = 0) {Z : C} (h_1 : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (h.liftK k hk) (CategoryTheory.CategoryStruct.comp h.i h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.sUnion : ∀ {α : Type u} {g : Set (Set α)} (S : Set (Set α)),
  (∀ s ∈ S, TopologicalSpace.GenerateOpen g s) → TopologicalSpace.GenerateOpen g (⋃₀ S)
-- Mathlib.Order.Partition.Finpartition
Finpartition.atomise_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, s.Nonempty → (Finpartition.atomise s ∅).parts = {s}
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- The lattice of intermediate fields is compactly generated.  -/
IntermediateField.instIsCompactlyGenerated : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  IsCompactlyGenerated (IntermediateField F E)
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.toOrderBot : {α : Type u_5} → [self : IdemSemiring α] → OrderBot α