mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.FinEnum.Option
_private.Mathlib.Data.FinEnum.Option.0.FinEnum.recEmptyOption.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (x = 0 → motive 0) → ((n : ℕ) → x = n.succ → motive n.succ) → motive x
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs is said to be preserved by localization
if `P` holds for `M⁻¹R →+* M⁻¹S` whenever `P` holds for `R →+* S`.  -/
RingHom.LocalizationPreserves : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_le_iff_le_map : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S],
  Function.Bijective ⇑f → ∀ {I : Ideal R} {K : Ideal S}, Ideal.comap f K ≤ I ↔ K ≤ Ideal.map f I
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instModule : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : Nonempty ι] →
                    [inst_5 : Semiring R] →
                      [inst_6 : (i : ι) → AddCommMonoid (G i)] →
                        [inst_7 : (i : ι) → Module R (G i)] →
                          [inst_8 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] →
                            Module R (DirectLimit G f)
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.posForm_apply_root_root_le_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) (i j : ι) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] [IsStrictOrderedRing S]
  (hi : optParam (P.root i ∈ Submodule.span S (Set.range ⇑P.root)) ⋯)
  (hj : optParam (P.root j ∈ Submodule.span S (Set.range ⇑P.root)) ⋯),
  (B.posForm ⟨P.root i, hi⟩) ⟨P.root j, hj⟩ ≤ 0 ↔ P.pairingIn S i j ≤ 0
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.tautologicalCocone'_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))),
  (CategoryTheory.Presheaf.tautologicalCocone' P).pt = P
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.comp_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : TypeCat.Fun Y Z) (g : TypeCat.Fun X Y) (a : X),
  (f.comp g) a = f.toFun (g.toFun a)
-- Mathlib.Data.Fin.Basic
/-- Equivalence between `Fin n` and `{ i // i < n }`.  -/
Fin.equivSubtype : {n : ℕ} → Fin n ≃ { i // i < n }
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.shift_comm_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} {τ : F₁ ⟶ F₂} {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    ∀ {Z : CategoryTheory.Functor C D} (h : F₂.comp (CategoryTheory.shiftFunctor D a) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₁ a).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight τ (CategoryTheory.shiftFunctor D a))
            h) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).whiskerLeft τ)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.commShiftIso F₂ a).hom h)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a `M → M → α` function to `MulArchimedeanClass M → MulArchimedeanClass M → α`.  -/
MulArchimedeanClass.lift₂ : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        {α : Type u_2} →
          (f : M → M → α) →
            (∀ (a₁ b₁ a₂ b₂ : M),
                MulArchimedeanClass.mk a₁ = MulArchimedeanClass.mk b₁ →
                  MulArchimedeanClass.mk a₂ = MulArchimedeanClass.mk b₂ → f a₁ a₂ = f b₁ b₂) →
              MulArchimedeanClass M → MulArchimedeanClass M → α
-- Init.System.ST
Void.mk : {σ : Type} → σ → Void σ
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- `F⟮x⟯ / F` is a purely inseparable extension if and only if the minimal polynomial of `x`
has separable degree one.  -/
IntermediateField.isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  IsPurelyInseparable F ↥F⟮x⟯ ↔ (minpoly F x).natSepDegree = 1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S hg c hc).iso =
    CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).H
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.mapRange_smul : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M]
  [inst_2 : Zero N] [inst_3 : SMulZeroClass R N] {f : M → N} {hf : f 0 = 0} (c : R) (v : α →₀ M),
  (∀ (x : M), f (c • x) = c • f x) → Finsupp.mapRange f hf (c • v) = c • Finsupp.mapRange f hf v
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `Quotient.locallyPathConnectedSpace`.

---

Quotients of locally path-connected spaces are locally path-connected.  -/
Quotient.locPathConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] {s : Setoid X},
  LocallyPathConnectedSpace (Quotient s)
-- Mathlib.Algebra.Group.Basic
dite_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul β α] (p : Prop) [inst_1 : Decidable p] (a : α) (b : p → β) (c : ¬p → β),
  (if h : p then b h else c h) • a = if h : p then b h • a else c h • a
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
Algebra.adjoin.powerBasis'.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x), Algebra.adjoin.powerBasis' hx = (AdjoinRoot.powerBasis' ⋯).map (minpoly.equivAdjoin hx)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv_assoc : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.OplaxLeftLinear C] (c c' : C) (d : D)
  {Z : D'}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') (F.obj d) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
          (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c' d))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).inv h)) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxLeftLinear.δₗ F (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d) h)
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- A multiplicative norm on a ring `R` is a multiplicative ring seminorm such that `f x = 0`
implies `x = 0`.

It is recommended to use `AbsoluteValue R ℝ` instead (which works for `Semiring R`
and is equivalent to `MulRingNorm R` for a nontrivial `Ring R`).  -/
MulRingNorm : (R : Type u_2) → [NonAssocRing R] → Type u_2
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.BoundaryLE.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (j : ι),
  e.BoundaryLE j = (c'.Rel (e.f j) (c'.next (e.f j)) ∧ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k))
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.CategoryWithHomology.hasHomology : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  [self : CategoryTheory.CategoryWithHomology C] (S : CategoryTheory.ShortComplex C), S.HasHomology
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_const : ∀ {M : Type u_2} [inst : CommMonoid M] (n : ℕ) (x : M), ∏ _i, x = x ^ n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
CategoryTheory.yonedaCommGrpGrp_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ X₂ : CategoryTheory.CommGrp C} (ψ : X₁ ⟶ X₂)
  (Y : (CategoryTheory.Grp C)ᵒᵖ),
  (CategoryTheory.yonedaCommGrpGrp.map ψ).app Y =
    CommGrpCat.ofHom { toFun := fun x => CategoryTheory.CategoryStruct.comp x ψ.hom, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.instFunLikeContinuousMapGeneratedBy : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [inst_1 : TopologicalSpace Y] →
          {Z : Type v'} → [inst_2 : TopologicalSpace Z] → FunLike (Topology.ContinuousMapGeneratedBy X Y Z) Y Z
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.le_norm : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] [inst_2 : LT α] [inst_3 : Std.IsPreorder α]
  [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α) (lhs rhs : Lean.Grind.CommRing.Expr)
  (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.core_cert lhs rhs p = true →
    Lean.Grind.CommRing.Expr.denote ctx lhs ≤ Lean.Grind.CommRing.Expr.denote ctx rhs →
      Lean.Grind.CommRing.Poly.denote ctx p ≤ 0
-- Mathlib.RepresentationTheory.Intertwining
Representation.IsIntertwiningMap.mk : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} {f : V →ₗ[A] W},
  (∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)) → ρ.IsIntertwiningMap σ f
-- Mathlib.Order.Interval.Finset.Basic
Finset.filter_lt_lt_eq_Ioo : ∀ {α : Type u_2} (a b : α) [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : Fintype α]
  [inst_3 : DecidablePred fun j => a < j ∧ j < b], {j | a < j ∧ j < b} = Finset.Ioo a b
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [inst_2 : SizeOf C] [inst_3 : SizeOf D] (app : (X : C) → F.obj X ⟶ G.obj X)
  (naturality :
    autoParam
      (∀ ⦃X Y : C⦄ (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (F.map f) (app Y) = CategoryTheory.CategoryStruct.comp (app X) (G.map f))
      CategoryTheory.NatTrans.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Plausible.Sampleable
Plausible.SampleableExt.mk : {α : Sort u} →
  (proxy : Type v) →
    [proxyRepr : Repr proxy] →
      [shrink : Plausible.Shrinkable proxy] →
        [sample : Plausible.Arbitrary proxy] → (proxy → α) → Plausible.SampleableExt α
-- Mathlib.Algebra.Homology.Factorizations.Basic
CochainComplex.degreewiseEpiWithInjectiveKernel_iff_of_isZero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L),
  CategoryTheory.Limits.IsZero L →
    (CochainComplex.degreewiseEpiWithInjectiveKernel f ↔ ∀ (n : ℤ), CategoryTheory.Injective (K.X n))
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.initialHom_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (d : CategoryTheory.Factorisation f),
  d.initialHom.h = d.ι
-- Std.Time.Time.PlainTime
Std.Time.instReprPlainTime.repr : Std.Time.PlainTime → ℕ → Std.Format
-- Mathlib.Topology.Compactness.SigmaCompact
/-- **Alias** of `CompactExhaustion.mem_sdiff_shiftr_find`. -/
CompactExhaustion.mem_diff_shiftr_find : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (x : X),
  x ∈ K.shiftr (K.find x + 1) \ K.shiftr (K.find x)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.coe_dualBasis : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι], ⇑b.dualBasis = b.coord
-- Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap
ContinuousLinearMap.isClosed_genEigenspace : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [T0Space M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] (f : M →L[R] M) (μ : R)
  (n : ℕ), IsClosed ↑((Module.End.genEigenspace (↑f) μ) ↑n)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MonadHorizontalComp.mk : {m : Type → Type} →
  [toMonadWhiskerRight : Mathlib.Tactic.BicategoryLike.MonadWhiskerRight m] →
    (Mathlib.Tactic.BicategoryLike.WhiskerRight →
        Mathlib.Tactic.BicategoryLike.HorizontalComp → m Mathlib.Tactic.BicategoryLike.HorizontalComp) →
      Mathlib.Tactic.BicategoryLike.MonadHorizontalComp m
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.ofLp_single : ∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] (i : ι)
  (a : β i), (PiLp.single p i a).ofLp = Pi.single i a
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_le_lift : ∀ {x : Cardinal.{v}} {m : ℕ∞}, ↑m ≤ Cardinal.lift.{u, v} x ↔ ↑m ≤ x
-- Mathlib.Data.List.Induction
List.twoStepInduction.eq_def : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (x : α) → motive [x])
  (cons_cons : (x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs))
  (l : List α),
  List.twoStepInduction nil singleton cons_cons l =
    match l with
    | [] => nil
    | [x] => singleton x
    | x :: y :: xs =>
      cons_cons x y xs (List.twoStepInduction nil singleton cons_cons xs) fun y =>
        List.twoStepInduction nil singleton cons_cons (y :: xs)
-- Init.Data.UInt.Bitwise
UInt32.zero_and : ∀ {a : UInt32}, 0 &&& a = 0
-- Mathlib.Logic.Equiv.Defs
/-- If `α ≃ β` and `β` is a singleton type, then so is `α`.  -/
Equiv.unique : {α : Sort u} → {β : Sort v} → [Unique β] → α ≃ β → Unique α
-- Mathlib.SetTheory.ZFC.Rank
PSet.lt_rank_iff : ∀ {o : Ordinal.{u_1}} {x : PSet.{u_1}}, o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.cancel_var_cert.eq_1 : ∀ (c : ℤ) (x : Lean.Grind.CommRing.Var) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.cancel_var_cert c x p₁ p₂ = (c != 0 && p₂.beq' (Lean.Grind.CommRing.Poly.cancelVar c x p₁))
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.isConj_iff_cycleType_eq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  IsConj σ τ ↔ σ.cycleType = τ.cycleType
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'_le_localized'_of_smul_le : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] {P Q : Submodule R M} (x : ↥p),
  x • P ≤ Q → Submodule.localized' S p f P ≤ Submodule.localized' S p f Q
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKey? k = m.getKey? k
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.nonUnitalStarAlgHom_postcomp_apply : ∀ (X : Type u_1) {M : Type u_3} {R : Type u_4} {S : Type u_5} [inst : Zero X] [inst_1 : CommSemiring M]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace S] [inst_5 : CommSemiring R]
  [inst_6 : StarRing R] [inst_7 : IsTopologicalSemiring R] [inst_8 : ContinuousStar R] [inst_9 : CommSemiring S]
  [inst_10 : StarRing S] [inst_11 : IsTopologicalSemiring S] [inst_12 : ContinuousStar S] [inst_13 : Module M R]
  [inst_14 : Module M S] [inst_15 : ContinuousConstSMul M R] [inst_16 : ContinuousConstSMul M S] (φ : R →⋆ₙₐ[M] S)
  (hφ : Continuous ⇑φ) (f : ContinuousMapZero X R),
  (ContinuousMapZero.nonUnitalStarAlgHom_postcomp X φ hφ) f =
    { toFun := ⇑φ, continuous_toFun := hφ, map_zero' := ⋯ }.comp f
-- Init.Data.Nat.Lemmas
/-- See `forall_lt_succ_right'` for a variant where `p` takes the bound as an argument.  -/
Nat.forall_lt_succ_right : ∀ {n : ℕ} {p : ℕ → Prop}, (∀ m < n + 1, p m) ↔ (∀ m < n, p m) ∧ p n
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_add_mul_tdiv : ∀ (a b : ℤ), a.tmod b + b * a.tdiv b = a
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instIsScalarTowerOfReal : ∀ {R : Type u_1} {R' : Type u_2} {E : Type u_3} [inst : Group E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ] [inst_4 : SMul R' ℝ] [inst_5 : SMul R' NNReal]
  [inst_6 : IsScalarTower R' NNReal ℝ] [inst_7 : SMul R R'] [IsScalarTower R R' ℝ], IsScalarTower R R' (GroupSeminorm E)
-- Mathlib.Topology.Algebra.Monoid
nhds_mul_nhds_one : ∀ {M : Type u_6} [inst : MulOneClass M] [inst_1 : TopologicalSpace M] [ContinuousMul M] (a : M),
  nhds a * nhds 1 = nhds a
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_differentiableOn_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G},
  DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s
-- Std.Time.Date.Unit.Week
/-- Convert `Minute.Offset` into `Week.Offset`.
 -/
Std.Time.Week.Offset.ofMinutes : Std.Time.Minute.Offset → Std.Time.Week.Offset
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q),
  CochainComplex.HomComplex.Cochain.fromSingleMk (f + g) h =
    CochainComplex.HomComplex.Cochain.fromSingleMk f h + CochainComplex.HomComplex.Cochain.fromSingleMk g h
-- Lean.Meta.Tactic.Grind.Split
/-- Pairs `(anchor, split)`  -/
Lean.Meta.Grind.SplitCandidateAnchors.candidates : Lean.Meta.Grind.SplitCandidateAnchors → Array Lean.Meta.Grind.SplitCandidateWithAnchor
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.map.match_1.eq_3 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithInitial C) → (X ⟶ Y) → Sort u_3)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1) →
        motive (CategoryTheory.WithInitial.of a) (CategoryTheory.WithInitial.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of a) →
        motive CategoryTheory.WithInitial.star (CategoryTheory.WithInitial.of a) x)
  (h_3 :
    (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star) →
      motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star x),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => h_2 a x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => h_3 x) =
    h_3 x
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a c < slope f a b`.  -/
map_lt_lineMap_iff_slope_lt_slope_left : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < r * (b - a) →
    (f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔
      slope f a ((AffineMap.lineMap a b) r) < slope f a b)
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Find the longest prefix of `n` such that `f` returns `some` (or return `none` otherwise).  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Lean.Name.findPrefix : {α : Type u_1} → (Lean.Name → Option α) → Lean.Name → Option α
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {f g : CompactlySupportedContinuousMap α β}, (∀ (x : α), f x = g x) → f = g
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond_succ_left : ∀ (n k : ℕ), k ≠ 0 → (n + 1).stirlingSecond k = k * n.stirlingSecond k + n.stirlingSecond (k - 1)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.yoneda_exact₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ {X : C} (f : T.obj₃ ⟶ X),
      CategoryTheory.CategoryStruct.comp T.mor₂ f = 0 → ∃ g, f = CategoryTheory.CategoryStruct.comp T.mor₃ g
-- Init.Data.List.Lemmas
List.filterMap_reverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α},
  List.filterMap f l.reverse = (List.filterMap f l).reverse
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lt_omega_iff_card_lt : ∀ {x o : Ordinal.{u_1}}, x < Ordinal.omega o ↔ x.card < Cardinal.aleph o