mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.equivHomsetLeftOfNatIso_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (iso : F ≅ F') {X : C} {Y : D} (f : F.obj X ⟶ Y),
  (CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso) f = CategoryTheory.CategoryStruct.comp (iso.inv.app X) f
-- Mathlib.Lean.MessageData.Trace
/-- Extract the instance name from a rendered `apply @Foo to Goal` trace header.
Returns the string between `"apply "` and `" to "`.

Note: this is fragile string matching against Lean's `Meta.synthInstance` trace format.
If the trace format changes, this function will silently return the original string.
Once [lean4#12699](https://github.com/leanprover/lean4/pull/12699) is available,
these nodes will have trace class `Meta.synthInstance.apply` and can be identified
structurally via `td.cls` instead of string-matching on the header.  -/
Lean.MessageData.extractInstName : String → String
-- Init.Data.UInt.IntToBitVec
Bool.toBitVec64_toUSize : ∀ {b : Bool} (h : System.Platform.numBits = 64), b.toUSize.toBitVec64 h = BitVec.setWidth 64 (BitVec.ofBool b)
-- Mathlib.Algebra.Group.TypeTags.Basic
instInhabitedAdditive : {α : Type u} → [Inhabited α] → Inhabited (Additive α)
-- Std.Data.DTreeMap.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.get : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → (t : Std.DTreeMap α β cmp) → (a : α) → a ∈ t → β a
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.LocallyDirected.ofIsBasisOpensRange_trans : ∀ {X : AlgebraicGeometry.Scheme} {𝒰 : X.OpenCover} [inst : Preorder 𝒰.I₀]
  (hle :
    ∀ {i j : 𝒰.I₀},
      i ≤ j ↔ AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i) ≤ AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f j))
  (H : TopologicalSpace.Opens.IsBasis (Set.range fun i => AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i))) {i j : 𝒰.I₀}
  (hij : i ≤ j),
  AlgebraicGeometry.Scheme.Cover.trans 𝒰 (CategoryTheory.homOfLE hij) =
    AlgebraicGeometry.IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) ⋯
-- Mathlib.Topology.Closure
interior_union_inter_interior_compl_left_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, interior (s ∪ t) ∩ interior sᶜ ⊆ interior t
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- `monomial s a` is the monomial `a * X ^ s`.  -/
SkewPolynomial.monomial : {R : Type u_1} → ℕ → [inst : Semiring R] → R →ₗ[R] SkewPolynomial R
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.comp.inj : ∀ {a a_1 a_2 a_3 : Turing.ToPartrec.Code}, a.comp a_1 = a_2.comp a_3 → a = a_2 ∧ a_1 = a_3
-- Init.Data.String.Slice
/-- Finds the position of the first match of the pattern `pat` in a slice `s`. If there
is no match `s.endPos` is returned.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".toSlice.find Char.isWhitespace).get! == ' '`

* `"tea".toSlice.find (fun (c : Char) => c == 'X') == "tea".toSlice.endPos`

* `("coffee tea water".toSlice.find "tea").get! == 't'`
 -/
String.Slice.find : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        (s : String.Slice) → (pat : ρ) → [String.Slice.Pattern.ToForwardSearcher pat σ] → s.Pos
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.mkOfOplax_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : CategoryTheory.Oplax.StrongTrans F.toOplax G.toOplax) (a : B),
  (CategoryTheory.Pseudofunctor.StrongTrans.mkOfOplax η).app a = η.app a
-- Mathlib.Topology.Separation.Hausdorff
/-- If the codomain of a topological embedding is a Hausdorff space, then so is its domain.
See also `T2Space.of_continuous_injective`.  -/
Topology.IsEmbedding.t2Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {f : X → Y},
  Topology.IsEmbedding f → T2Space X
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenrange_nat : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, f.genEigenrange μ ↑k = ((f - μ • 1) ^ k).range
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Find an element in the tree using a cut function.  -/
RBTree.RBSet.findP? : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Ordering) → Option α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_decl_eq : ∀ {w : ℕ} {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} (curr : ℕ) (s : aig.RefVec curr) (a : ℕ) (hcurr : curr ≤ w)
  (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).aig.decls[idx] = aig.decls[idx]
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.instMin : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] → [inst_3 : Module A W] → {ρ : Representation A G W} → Min (Subrepresentation ρ)
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.toReal : ∀ {p q : ENNReal}, 1 < p.toReal → ∀ [p.HolderConjugate q], p.toReal.HolderConjugate q.toReal
-- Mathlib.Topology.Category.TopCat.Opens
Topology.IsOpenEmbedding.functor_obj_iInf : ∀ {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {ι : Type u_1}
  [Nonempty ι] [Finite ι] (g : ι → TopologicalSpace.Opens ↑X), hf.functor.obj (⨅ i, g i) = ⨅ i, hf.functor.obj (g i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.entryAtIdx!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {i : ℕ} [inst : Inhabited ((a : α) × β a)], t₁.entryAtIdx! i = t₂.entryAtIdx! i
-- Mathlib.Order.Bounds.Basic
IsLeast.nonempty : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLeast s a → s.Nonempty
-- Mathlib.Analysis.CStarAlgebra.Unitary.Span
/-- For `a` selfadjoint with `‖a‖ ≤ 1`, this is the unitary `a + I • √(1 - a ^ 2)`.  -/
selfAdjoint.unitarySelfAddISMul : {A : Type u_1} →
  [inst : CStarAlgebra A] →
    [inst_1 : PartialOrder A] → [StarOrderedRing A] → (a : ↥(selfAdjoint A)) → ‖a‖ ≤ 1 → ↥(unitary A)
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_comp_coyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare) {A : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} A] (P : CategoryTheory.Functor Cᵒᵖ A),
  S.SheafCondition P ↔ ∀ (X : Aᵒᵖ), S.SheafCondition (P.comp (CategoryTheory.coyoneda.obj X))
-- Mathlib.GroupTheory.OrderOfElement
Commute.orderOf_mul_eq_mul_orderOf_of_coprime : ∀ {G : Type u_1} [inst : Monoid G] {x y : G},
  Commute x y → (orderOf x).Coprime (orderOf y) → orderOf (x * y) = orderOf x * orderOf y
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.mk.inj : ∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {P Q pt : C} {fst : pt ⟶ P} {snd : pt ⟶ Q} {inl : P ⟶ pt} {inr : Q ⟶ pt}
  {inl_fst :
    autoParam (CategoryTheory.CategoryStruct.comp inl fst = CategoryTheory.CategoryStruct.id P)
      CategoryTheory.Limits.BinaryBicone.inl_fst._autoParam}
  {inl_snd :
    autoParam (CategoryTheory.CategoryStruct.comp inl snd = 0) CategoryTheory.Limits.BinaryBicone.inl_snd._autoParam}
  {inr_fst :
    autoParam (CategoryTheory.CategoryStruct.comp inr fst = 0) CategoryTheory.Limits.BinaryBicone.inr_fst._autoParam}
  {inr_snd :
    autoParam (CategoryTheory.CategoryStruct.comp inr snd = CategoryTheory.CategoryStruct.id Q)
      CategoryTheory.Limits.BinaryBicone.inr_snd._autoParam}
  {pt_1 : C} {fst_1 : pt_1 ⟶ P} {snd_1 : pt_1 ⟶ Q} {inl_1 : P ⟶ pt_1} {inr_1 : Q ⟶ pt_1}
  {inl_fst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inl_1 fst_1 = CategoryTheory.CategoryStruct.id P)
      CategoryTheory.Limits.BinaryBicone.inl_fst._autoParam}
  {inl_snd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inl_1 snd_1 = 0)
      CategoryTheory.Limits.BinaryBicone.inl_snd._autoParam}
  {inr_fst_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inr_1 fst_1 = 0)
      CategoryTheory.Limits.BinaryBicone.inr_fst._autoParam}
  {inr_snd_1 :
    autoParam (CategoryTheory.CategoryStruct.comp inr_1 snd_1 = CategoryTheory.CategoryStruct.id Q)
      CategoryTheory.Limits.BinaryBicone.inr_snd._autoParam},
  { pt := pt, fst := fst, snd := snd, inl := inl, inr := inr, inl_fst := inl_fst, inl_snd := inl_snd,
        inr_fst := inr_fst, inr_snd := inr_snd } =
      { pt := pt_1, fst := fst_1, snd := snd_1, inl := inl_1, inr := inr_1, inl_fst := inl_fst_1, inl_snd := inl_snd_1,
        inr_fst := inr_fst_1, inr_snd := inr_snd_1 } →
    pt = pt_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1 ∧ inl ≍ inl_1 ∧ inr ≍ inr_1
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.instQuotientIdeal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (I : Ideal S)
  [Algebra.QuasiFinite R S], Algebra.QuasiFinite R (S ⧸ I)
-- Mathlib.Computability.MyhillNerode
Language.start_toDFA : ∀ {α : Type u} (L : Language α), ↑L.toDFA.start = L
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.toFinsupp_algebraMap : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  ((algebraMap R (Polynomial A)) r).toFinsupp = (algebraMap R (AddMonoidAlgebra A ℕ)) r
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.key : Lean.Meta.SynthInstance.GeneratorNode → Lean.Expr
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.Hom.mk.injEq : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} (app : (X : C) → (Y : D) → P.obj X Y ⟶ Q.obj X Y)
  (naturality :
    autoParam
      (∀ ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y'),
        CategoryTheory.CategoryStruct.comp (P.map f g) (app X' Y) =
          CategoryTheory.CategoryStruct.comp (app X Y') (Q.map f g))
      CategoryTheory.ProfunctorCore.Hom.naturality._autoParam)
  (app_1 : (X : C) → (Y : D) → P.obj X Y ⟶ Q.obj X Y)
  (naturality_1 :
    autoParam
      (∀ ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y'),
        CategoryTheory.CategoryStruct.comp (P.map f g) (app_1 X' Y) =
          CategoryTheory.CategoryStruct.comp (app_1 X Y') (Q.map f g))
      CategoryTheory.ProfunctorCore.Hom.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The arrow in the ReflQuiver `OneTruncation₂ V` of a 2-truncated simplicial set arising from the
1st face of a 2-simplex.  -/
SSet.Truncated.ev02₂ : {V : SSet.Truncated 2} →
  (φ : V.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 })) →
    SSet.Truncated.ev0₂ φ ⟶ SSet.Truncated.ev2₂ φ
-- Mathlib.Data.List.OfFn
/-- Note we can only state this when the two functions are indexed by defeq `n`.  -/
List.ofFn_injective : ∀ {α : Type u} {n : ℕ}, Function.Injective List.ofFn
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.degBound.eq_def : ∀ (k : ℕ) (D : ℕ → ℕ) (x : ℕ),
  ChevalleyThm.MvPolynomialC.degBound k D x =
    match x with
    | 0 => 1
    | n.succ =>
      ChevalleyThm.MvPolynomialC.numBound k D (n + 1) ^ ChevalleyThm.MvPolynomialC.numBound k D (n + 1) *
        ChevalleyThm.MvPolynomialC.degBound k D n
-- Mathlib.Probability.Kernel.SetIntegral
ProbabilityTheory.Kernel.integral_integral_indicator : ∀ {X : Type u_1} {Y : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (κ : ProbabilityTheory.Kernel X Y)
  (μ : MeasureTheory.Measure X) (f : X → Y → E) {s : Set X},
  MeasurableSet s →
    ∫ (x : X), ∫ (y : Y), s.indicator (fun x => f x y) x ∂κ x ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂κ x ∂μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option (β k) → Option (β k)}, m.WF → (k ∈ m.alter k f ↔ (f (m.get? k)).isSome = true)
-- Init.Control.ExceptCps
ExceptCpsT.runCatch_lift : ∀ {m : Type u → Type u_1} {α : Type u} [inst : Monad m] [LawfulMonad m] (x : m α), (ExceptCpsT.lift x).runCatch = x
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofBaseOfFinite_finite : ∀ {α : Type u_1} {E : Set α} (hE : E.Finite) (IsBase : Set α → Prop) (exists_isBase : ∃ B, IsBase B)
  (isBase_exchange : Matroid.ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  (Matroid.ofIsBaseOfFinite hE IsBase exists_isBase isBase_exchange subset_ground).Finite
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.Scheme.Hom.isClosedMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.UniversallyClosed f], IsClosedMap ⇑f
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- A rank-one operator on an inner product space is given by `x ↦ y ↦ z ↦ ⟪y, z⟫ • x`.

This is also sometimes referred to as an outer product of vectors on a Hilbert space.
This corresponds to the matrix outer product `Matrix.vecMulVec`, see
`InnerProductSpace.toMatrix_rankOne` and `InnerProductSpace.symm_toEuclideanLin_rankOne` in
`Mathlib/Analysis/InnerProductSpace/PiL2.lean`.  -/
InnerProductSpace.rankOne : (𝕜 : Type u_4) →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : RCLike 𝕜] →
        [inst_1 : SeminormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : SeminormedAddCommGroup F] → [inst_4 : InnerProductSpace 𝕜 F] → E →L[𝕜] F →L⋆[𝕜] F →L[𝕜] E
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
GaussianFourier.integral_rexp_neg_mul_sq_norm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {b : ℝ},
  0 < b → ∫ (v : V), Real.exp (-b * ‖v‖ ^ 2) = (Real.pi / b) ^ (↑(Module.finrank ℝ V) / 2)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_subLeft_nhdsNE : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {c a : G},
  Filter.map (fun x => c - x) (nhdsWithin a {a}ᶜ) = nhdsWithin (c - a) {c - a}ᶜ
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- The head of an `m`-admissible list.  -/
SimplexCategoryGenRel.IsAdmissible.head : {m a : ℕ} → {L : List ℕ} → SimplexCategoryGenRel.IsAdmissible m (a :: L) → Fin (m + 1)
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.lt.injEq : ∀ (lhs rhs : ℕ) (proof : Lean.Expr) (lhs_1 rhs_1 : ℕ) (proof_1 : Lean.Expr),
  (Mathlib.Tactic.Order.AtomicFact.lt lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.lt lhs_1 rhs_1 proof_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1)
-- Mathlib.Topology.MetricSpace.Cauchy
/-- A variation around the pseudometric characterization of Cauchy sequences  -/
Metric.cauchySeq_iff' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α},
  CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_map_left_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) {X Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G}
  (g : X ⟶ Y), ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).map g).left.right = g.right
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
isMIntegralCurve_iff_isMIntegralCurveOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x}, IsMIntegralCurve γ v ↔ IsMIntegralCurveOn γ v Set.univ
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinter_le_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s.ndinter t ≤ s
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.head_supports : ∀ {S : Finset Turing.PartrecToTM2.Λ'} {k : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Λ'.Supports S q → Turing.PartrecToTM2.Λ'.Supports S (Turing.PartrecToTM2.head k q)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.abs_integral_le_integral_abs : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ}, a ≤ b → |∫ (x : ℝ) in a..b, f x ∂μ| ≤ ∫ (x : ℝ) in a..b, |f x| ∂μ
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.hasLimits : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.HasLimits (ModuleCat R)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains'.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k' : α) →
                (v : β k') →
                  (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v l r)) →
            motive l
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The wreath product of group `G` iterated `n` times.  -/
IteratedWreathProduct : Type u → ℕ → Type u
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_subtypeDomain_index : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : Zero M] {p : α → Prop} [inst_1 : AddCommMonoid N] {v : α →₀ M}
  {h : α → M → N}, (∀ x ∈ v.support, p x) → ((Finsupp.subtypeDomain p v).sum fun a b => h (↑a) b) = v.sum h
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.instIsNontrivial : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  [hv : v.RankOne], v.IsNontrivial
-- Mathlib.Analysis.SpecialFunctions.Choose
/-- `n.choose k` is big-theta `n^k`.  -/
isTheta_choose : ∀ (k : ℕ), (fun n => ↑(n.choose k)) =Θ[Filter.atTop] fun n => ↑n ^ k
-- Mathlib.Order.Sublattice
Sublattice.mk_le_mk : ∀ {α : Type u_2} [inst : Lattice α] {s t : Set α} (hs_sup : SupClosed s) (hs_inf : InfClosed s) (ht_sup : SupClosed t)
  (ht_inf : InfClosed t),
  { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } ≤
      { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔
    s ⊆ t
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
_private.Mathlib.MeasureTheory.VectorMeasure.BoundedVariation.0.BoundedVariationOn.instIsFiniteMeasureMeasureAux : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ), MeasureTheory.IsFiniteMeasure (BoundedVariationOn.measureAux✝ hf)
-- Aesop.Util.Basic
/-- Partition an array of structures containing `MVarId`s into 'goals' and
'proper mvars'. An `MVarId` from the input array `goals` is classified as a
proper mvar if any of the `MVarId`s depend on it, and as a goal otherwise.
Additionally, for each goal, we report the set of mvars that the goal depends
on.
 -/
Aesop.partitionGoalsAndMVars : {α : Type} →
  (α → Lean.MVarId) →
    Array α → Lean.MetaM (Array (α × Aesop.UnorderedArraySet Lean.MVarId) × Aesop.UnorderedArraySet Lean.MVarId)
-- Mathlib.Tactic.FunProp.Theorems
/-- For a theorem declaration `declName` return `fun_prop` theorem. It correctly detects which
type of theorem it is.  -/
Mathlib.Meta.FunProp.getTheoremFromConst : Lean.Name → optParam ℕ 1000 → Lean.MetaM Mathlib.Meta.FunProp.Theorem
-- Mathlib.FieldTheory.LinearDisjoint
/-- If there exists an `F`-basis of `B` which remains linearly independent over `A`, then
`A` and `B` are linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_basis_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  {ι : Type u_1} (b : Module.Basis ι F ↥B), LinearIndependent (↥A) (⇑B.val ∘ ⇑b) → A.LinearDisjoint ↥B
-- Mathlib.Logic.Pairwise
Pairwise.of_comp_of_surjective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : β → α},
  Pairwise (Function.onFun r f) → Function.Surjective f → Pairwise r
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_Ici : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : Preorder α]
  {a : α} {μ : MeasureTheory.Measure α} [ClosedIciTopology α], MeasureTheory.NullMeasurableSet (Set.Ici a) μ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Functor.mapExtLinearMap_toAddMonoidHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (R : Type u_1) [inst_9 : Ring R]
  [inst_10 : CategoryTheory.Linear R C] [inst_11 : CategoryTheory.Linear R D]
  [inst_12 : CategoryTheory.Functor.Linear R F], ↑(F.mapExtLinearMap R X Y n) = F.mapExtAddHom X Y n
-- Mathlib.Algebra.Lie.Nilpotent
LieIdeal.lowerCentralSeries_map_eq : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (k : ℕ) {f : L →ₗ⁅R⁆ L'},
  Function.Surjective ⇑f →
    LieIdeal.map f (LieModule.lowerCentralSeries R L L k) = LieModule.lowerCentralSeries R L' L' k
-- Mathlib.NumberTheory.ArithmeticFunction.Liouville
/-- The Liouville function `λ(n)` defined to be `1` if `n` has an even number of prime factors
(counting multiplicity) and `-1` otherwise.  -/
ArithmeticFunction.liouville : ArithmeticFunction ℤ
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instPartialOrder : {G : Type u_1} → [inst : Group G] → PartialOrder (FiniteIndexNormalSubgroup G)
-- Mathlib.Order.Cover
/-- **Alias** of the forward direction of `covBy_iff_le_iff_lt_left`. -/
CovBy.le_iff_lt_left : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α}, x ⋖ y → ∀ {z : α}, z ≤ x ↔ z < y
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.find?_toList_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k : α} {v : β k}, List.find? (fun x => x.fst == k) m.toList = some ⟨k, v⟩ ↔ m.get? k = some v
-- Init.Data.UInt.Bitwise
UInt32.not_or_self : ∀ {a : UInt32}, ~~~a ||| a = -1