mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.mk.inj : ∀ {α : Type u} {toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α}
  {ord :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this := toPreorderOfLEArgs.decidableLE;
      Ord α)
      Std.Packages.LinearPreorderOfLEArgs.ord._autoParam}
  {le_total : autoParam (∀ (a b : α), a ≤ b ∨ b ≤ a) Std.Packages.LinearPreorderOfLEArgs.le_total._autoParam}
  {isLE_compare :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this_1 := toPreorderOfLEArgs.decidableLE;
      let this_2 := ord;
      ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b)
      Std.Packages.LinearPreorderOfLEArgs.isLE_compare._autoParam}
  {isGE_compare :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      let this_1 := toPreorderOfLEArgs.decidableLE;
      have this_2 := le_total;
      let this_3 := ord;
      ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a)
      Std.Packages.LinearPreorderOfLEArgs.isGE_compare._autoParam}
  {toPreorderOfLEArgs_1 : Std.Packages.PreorderOfLEArgs α}
  {ord_1 :
    autoParam
      (let this := toPreorderOfLEArgs_1.le;
      let this := toPreorderOfLEArgs_1.decidableLE;
      Ord α)
      Std.Packages.LinearPreorderOfLEArgs.ord._autoParam}
  {le_total_1 : autoParam (∀ (a b : α), a ≤ b ∨ b ≤ a) Std.Packages.LinearPreorderOfLEArgs.le_total._autoParam}
  {isLE_compare_1 :
    autoParam
      (let this := toPreorderOfLEArgs_1.le;
      let this_1 := toPreorderOfLEArgs_1.decidableLE;
      let this_2 := ord_1;
      ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b)
      Std.Packages.LinearPreorderOfLEArgs.isLE_compare._autoParam}
  {isGE_compare_1 :
    autoParam
      (let this := toPreorderOfLEArgs_1.le;
      let this_1 := toPreorderOfLEArgs_1.decidableLE;
      have this_2 := le_total_1;
      let this_3 := ord_1;
      ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a)
      Std.Packages.LinearPreorderOfLEArgs.isGE_compare._autoParam},
  { toPreorderOfLEArgs := toPreorderOfLEArgs, ord := ord, le_total := le_total, isLE_compare := isLE_compare,
        isGE_compare := isGE_compare } =
      { toPreorderOfLEArgs := toPreorderOfLEArgs_1, ord := ord_1, le_total := le_total_1,
        isLE_compare := isLE_compare_1, isGE_compare := isGE_compare_1 } →
    toPreorderOfLEArgs = toPreorderOfLEArgs_1 ∧ ord = ord_1
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.finite_of_toPiLocalization_pi_surjective : ∀ {ι : Type u_5} {R : ι → Type u_4} [inst : (i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)],
  Function.Surjective ⇑(PrimeSpectrum.toPiLocalization ((i : ι) → R i)) → Finite ι
-- Mathlib.Data.List.Defs
List.map₂Left.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (x : List β), List.map₂Left f [] x = []
-- Init.Data.Array.Extract
Array.any_popWhile : ∀ {α : Type u_1} {p : α → Bool} {as : Array α}, ((Array.popWhile p as).any fun a => !p a) = !as.all p
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_eq_tsum_of_ne_zero_bij : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : γ → α} (i : ↑(Function.support g) → β),
  Function.Injective i →
    Function.support f ⊆ Set.range i →
      (∀ (x : ↑(Function.support g)), f (i x) = g ↑x) → ∑' (x : β), f x = ∑' (y : γ), g y
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_rightUnitor_hom_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X
        (CategoryTheory.CategoryStruct.id
                (Opposite.op
                  (CategoryTheory.Comon.MonOpOpToComonObj
                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit
                        (CategoryTheory.Mon Cᵒᵖ))).ComonToMonOpOpObj)).unop.hom.unop)
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.not_isMulCommutative : ∀ (G : Type u_1) [inst : Group G] [Nontrivial G] [Group.IsPerfect G], ¬IsMulCommutative G
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.inf : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] [inst_1 : SemilatticeInf M] {f g : α → M},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport fun a => f a ⊓ g a
-- Init.Data.String.Basic
String.utf8ByteSize_toSlice : ∀ {s : String}, s.toSlice.utf8ByteSize = s.utf8ByteSize
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.addParam : Lean.IR.LocalContext → Lean.IR.Param → Lean.IR.LocalContext
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_left_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l},
  Lean.Order.meet P (Lean.Order.meet Q R) = Lean.Order.meet Q (Lean.Order.meet P R)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {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) (e : c.Embedding c') {i j k : ι}
  {i' j' k' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hi' : c'.prev j' = i'),
  c.next j = k →
    c'.next j' = k' →
      ∀ (cocone : CategoryTheory.Limits.CokernelCofork (K.d i j)) (hcocone : CategoryTheory.Limits.IsColimit cocone)
        ⦃W : C⦄ (φ : W ⟶ cocone.pt),
        CategoryTheory.CategoryStruct.comp φ (hcocone.desc (CategoryTheory.Limits.CokernelCofork.ofπ (K.d j k) ⋯)) = 0 ↔
          CategoryTheory.CategoryStruct.comp φ
              ((HomologicalComplex.extend.rightHomologyData.isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc
                (CategoryTheory.Limits.CokernelCofork.ofπ ((K.extend e).d j' k') ⋯)) =
            0