mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.rw : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β},
  f =ᶠ[l] g → ∀ (p : α → β → Prop), (∀ᶠ (x : α) in l, p x (f x)) → ∀ᶠ (x : α) in l, p x (g x)
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.mem_restrictTotalDegree : ∀ (σ : Type u) {R : Type v} [inst : CommSemiring R] (m : ℕ) (p : MvPolynomial σ R),
  p ∈ MvPolynomial.restrictTotalDegree σ R m ↔ p.totalDegree ≤ m
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_neg' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp (-a) b = -(toIcoDiv hp a (-b) + 1)
-- Lean.Meta.WHNF
/-- Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
expand let-expressions, expand assigned meta-variables, unfold aux declarations.
 -/
Lean.Meta.whnfCore : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Subobject.Basic
/-- For any morphism `f : X ⟶ Y` and subobject `y` of `Y`, `Subobject.pullbackπ f y` is the first
projection in the following pullback square:

```
(Subobject.pullback f).obj y ----pullbackπ f y---> (y : C)
         |                                            |
((Subobject.pullback f).obj y).arrow               y.arrow
         |                                            |
         v                                            v
         X ---------------------f-------------------> Y
```

For instance in the category of sets, `Subobject.pullbackπ f y` is the restriction of `f` to
elements of `X` that are in the preimage of `y ⊆ Y`.
 -/
CategoryTheory.Subobject.pullbackπ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        (f : X ⟶ Y) →
          (y : CategoryTheory.Subobject Y) →
            CategoryTheory.Subobject.underlying.obj ((CategoryTheory.Subobject.pullback f).obj y) ⟶
              CategoryTheory.Subobject.underlying.obj y
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.zero_apply : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)}, ⇑0 = 0
-- Init.Data.Array.Lemmas
Array.size_setIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α}, (xs.setIfInBounds i a).size = xs.size
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyι_comp_fromOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i] {Z : C}
  (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.fromOpcycles i j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Data.FunLike.Basic
/-- The class `FunLike F α β` (`Fun`ction-`Like`) expresses that terms of type `F`
have an injective coercion to functions from `α` to `β`.
`FunLike` is the non-dependent version of `DFunLike`.
This typeclass is used in the definition of the homomorphism typeclasses,
such as `ZeroHomClass`, `MulHomClass`, `MonoidHomClass`, ....
 -/
FunLike : Sort u_1 → Sort u_2 → Sort u_3 → Sort (max (max (max 1 u_1) u_2) u_3)
-- Lean.Environment
/-- Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration
tasks unless necessary. This can usually be done efficiently because `addConstAsync` ensures that
declarations added in an environment branch have that branch's declaration name as a prefix, so we
know exactly what tasks to wait for to find a declaration. However, this is not true for
declarations from `realizeConst`, which are not restricted to the current prefix, and reference to
which may escape the branch(es) they have been realized on such as when looking into the type `Expr`
of a declaration found on another branch. Thus when we cannot find the declaration using the fast
prefix-based lookup, we fall back to waiting for and looking at the realizations from all branches.
To avoid this expensive search for realizations from other branches, `skipRealize` can be set to ensure
negative lookups are as fast as positive ones.

Use `findTask` instead if any blocking should be avoided.
 -/
Lean.Environment.findAsync? : Lean.Environment → Lean.Name → optParam Bool false → Option Lean.AsyncConstantInfo
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α) (h : s.Terminates), s.length h = Nat.find h
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also `rnDeriv_smul_right`, which has no hypothesis on `μ` but requires finite `ν`.  -/
MeasureTheory.Measure.rnDeriv_smul_right' : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν]
  [MeasureTheory.SigmaFinite μ] {r : NNReal}, r ≠ 0 → ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [IsEmpty β], ∏'[L] (b : β), f b = 1
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.toFinsupp_symm_single : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (c : A) (z : L), ((LieAlgebra.LoopAlgebra.toFinsupp R A L).symm fun₀ | c => z) = AddMonoidAlgebra.single c 1 ⊗ₜ[R] z
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Topology.Inseparable
Specializes.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x y : X), x ⤳ y = (nhds x ≤ nhds y)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.copy_eq : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = ↑S),
  S.copy s hs = S
-- Batteries.Data.List.Basic
List.dropSliceTR.go.eq_def : ∀ {α : Type u_1} (l : List α) (m : ℕ) (a : List α) (a_1 : ℕ) (a_2 : Array α),
  List.dropSliceTR.go l m a a_1 a_2 =
    match a, a_1, a_2 with
    | [], x, x_1 => l
    | head :: xs, 0, acc => acc.toListAppend (List.drop m xs)
    | x :: xs, n.succ, acc => List.dropSliceTR.go l m xs n (acc.push x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.filter_eq_self_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool},
  Std.ExtDTreeMap.filter f t = t ↔ ∀ (k : α) (h : k ∈ t), f (t.getKey k h) (Std.ExtDTreeMap.Const.get t k h) = true
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowMatcher.addBelowPattern : Array Lean.Expr →
  ℕ →
    Lean.Name → ℕ → Lean.Meta.Match.AltLHS → Lean.MetaM (Lean.Meta.Match.AltLHS × Array Lean.Meta.IndPredBelow.NewDecl✝)
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- **Alias** of `MulHomClass.isMulFreimanHom`. -/
MonoidHomClass.isMulFreimanHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β}
  {n : ℕ} [inst_2 : FunLike F α β] [MulHomClass F α β] (f : F), Set.MapsTo (⇑f) A B → IsMulFreimanHom n A B ⇑f
-- Mathlib.CategoryTheory.Comma.Final
CategoryTheory.Comma.initial_snd : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [L.Initial], (CategoryTheory.Comma.snd L R).Initial
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.getElem_toArray_eq : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {r : Std.Roc α} {i : ℕ} {h : i < r.toArray.size},
  r.toArray[i] = (Std.PRange.succMany? (i + 1) r.lower).get ⋯
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.isTransitive_vonNeumann : ∀ (o : Ordinal.{u_1}), (ZFSet.vonNeumann o).IsTransitive
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GCommSemiring.mk : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddCommMonoid ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        [toGSemiring : DirectSum.GSemiring A] → (∀ (a b : GradedMonoid A), a * b = b * a) → DirectSum.GCommSemiring A
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C (CategoryTheory.CommMon D)) (X : C),
  (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).X.obj X = (F.obj X).X
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipSuffixWhile_eq_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, s.endsWith pat = false → s.skipSuffixWhile pat = s.endPos
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
/-- The product of generated σ-algebras is the one generated by rectangles, if both generating sets
are countably spanning.  -/
generateFrom_prod_eq : ∀ {α : Type u_3} {β : Type u_4} {C : Set (Set α)} {D : Set (Set β)},
  IsCountablySpanning C →
    IsCountablySpanning D →
      Prod.instMeasurableSpace = MeasurableSpace.generateFrom (Set.image2 (fun x1 x2 => x1 ×ˢ x2) C D)
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_two_iff : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] {f : Polynomial R},
  f.IsMonicOfDegree 2 ↔ ∃ a b, f = Polynomial.X ^ 2 + Polynomial.C a * Polynomial.X + Polynomial.C b
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- Given a measure space with an action of a finite group `G`, the measure of any `G`-invariant set
is determined by the measure of its intersection with a fundamental domain for the action of `G`.  -/
MeasureTheory.IsFundamentalDomain.measure_eq_card_smul_of_smul_ae_eq_self : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G]
  [Finite G],
  MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), (∀ (g : G), g • t =ᵐ[μ] t) → μ t = Nat.card G • μ (t ∩ s)
-- Mathlib.Algebra.Quaternion
/-- Multiplication is given by

* `1 * x = x * 1 = x`;
* `i * i = c₁ + c₂ * i`;
* `j * j = c₃`;
* `i * j = k`, `j * i = c₂ * j - k`;
* `k * k = - c₁ * c₃`;
* `i * k = c₁ * j + c₂ * k`, `k * i = -c₁ * j`;
* `j * k = c₂ * c₃ - c₃ * i`, `k * j = c₃ * i`.  -/
QuaternionAlgebra.instMul : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Ring R] → Mul (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_incidenceFinset_eq_degree : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : DecidableEq V],
  (G.incidenceFinset v).card = G.degree v
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuous_dom_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {f : CompactCoherentification X → Y},
  Continuous f ↔ ∀ (K : Set X), IsCompact K → ContinuousOn (f ∘ ⇑(CompactCoherentification.mk X)) K
-- Mathlib.Data.List.Intervals
List.Ico.notMem_top : ∀ {n m : ℕ}, m ∉ List.Ico n m
-- Mathlib.Tactic.Translate.Reorder
/-- Return the inverse permutation.  -/
Mathlib.Tactic.Translate.Permutation.reverse : Mathlib.Tactic.Translate.Permutation → Mathlib.Tactic.Translate.Permutation
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_arrow_eq_zero_iff : ∀ {α : Type u} {β' : Type v}, Cardinal.mk (α → β') = 0 ↔ Cardinal.mk α ≠ 0 ∧ Cardinal.mk β' = 0
-- Lean.Meta.Match.MatcherInfo
/-- Tag extension for declarations that should be inlined like matchers during LCNF conversion,
but are not matchers themselves (e.g. the `.het` auxiliaries from `mkCasesOnSameCtor`).
 -/
Lean.Meta.matcherLikeExt : Lean.TagDeclarationExtension
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.symmetricIco.eq_1 : ∀ (G : Type u_1) [inst : Neg G] [inst_1 : Preorder G] [inst_2 : LocallyFiniteOrder G],
  SummationFilter.symmetricIco G = { filter := Filter.map (fun N => Finset.Ico (-N) N) Filter.atTop }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α}, Std.DTreeMap.Raw.Const.get? t a = t.get? a
-- Mathlib.Tactic.Attr.Register
/-- The simpset `pull_end` translates algebraic formulations of endomorphisms into the standard
formulation of homomorphisms, so for example `1 : Equiv α α` becomes `Equiv.refl α` and
`a * b` becomes `b.trans a`.

The dual simpset is `push_end`.
 -/
Parser.Attr.pull_end : Lean.ParserDescr
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.algHom_ext_iff : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {I : Ideal A} [inst_5 : I.IsPrime] {f g : I.ResidueField →ₐ[R] B},
  f = g ↔ f.comp (IsScalarTower.toAlgHom R A I.ResidueField) = g.comp (IsScalarTower.toAlgHom R A I.ResidueField)
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.tensorProduct_compatibleSMul : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] (M₁ : Type u_5) (M₂ : Type u_6) [inst_4 : AddCommMonoid M₁]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M₁] [inst_7 : Module R M₂] [inst_8 : Module A M₁]
  [inst_9 : Module A M₂] [IsScalarTower R A M₁] [IsScalarTower R A M₂], TensorProduct.CompatibleSMul R A M₁ M₂
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.map_equiv : ∀ {ι' : Type u_2} {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12}
  [inst_1 : Semiring R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module R M'] (b : Module.Basis ι R M)
  (b' : Module.Basis ι' R M') (e : ι ≃ ι'), b.map (b.equiv b' e) = b'.reindex e.symm
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelpParams.fromJson : Lean.Json → Except String Lean.Lsp.SignatureHelpParams
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoX₂_hom_inv_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hg : S.g = 0),
  CategoryTheory.CategoryStruct.comp S.iCycles (S.cyclesIsoX₂ hg).inv = CategoryTheory.CategoryStruct.id S.cycles
-- Lean.Widget.Basic
Lean.Widget.instTypeNameContextInfo : TypeName Lean.Elab.ContextInfo
-- Mathlib.RingTheory.IsTensorProduct
Algebra.pushoutDesc_apply : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [H : Algebra.IsPushout R S R' S'] {A : Type u_8} [inst_11 : Semiring A] [inst_12 : Algebra R A] (f : S →ₐ[R] A)
  (g : R' →ₐ[R] A) (hf : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : S'),
  (Algebra.pushoutDesc S' f g hf) x = (Algebra.TensorProduct.lift f g hf) ((Algebra.IsPushout.equiv R S R' S').symm x)
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesParams.mk.inj : ∀ {changes changes_1 : Array Lean.Lsp.FileEvent},
  { changes := changes } = { changes := changes_1 } → changes = changes_1
-- Lean.Parser.Extension
/-- Reference to a parser declaration in the environment.  A `(Trailing)ParserDescr` if `isDescr` is
true.
 -/
Lean.Parser.ParserResolution.parser : Lean.Name → Bool → Lean.Parser.ParserResolution
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.homOverEquiv_apply : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) {X : AlgebraicGeometry.Scheme} [inst : X.Over S]
  (f : { f // AlgebraicGeometry.Scheme.Hom.IsOver f S }) (i : n),
  (AlgebraicGeometry.AffineSpace.homOverEquiv S) f i =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop ↑f))
      (AlgebraicGeometry.AffineSpace.coord S i)
-- Mathlib.Data.List.Forall2
List.SublistForall₂.below.cons : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  {motive : (a : List α) → (a_1 : List β) → List.SublistForall₂ R a a_1 → Prop} {a₁ : α} {a₂ : β} {l₁ : List α}
  {l₂ : List β} (a : R a₁ a₂) (a_1 : List.SublistForall₂ R l₁ l₂),
  List.SublistForall₂.below a_1 → motive l₁ l₂ a_1 → List.SublistForall₂.below ⋯
-- Init.Data.UInt.Bitwise
UInt64.toBitVec_shiftRight : ∀ (a b : UInt64), (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 64)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) =
    CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedElabHeaderResult.default : Lean.Elab.Command.ElabHeaderResult
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- The `G`-valued integral of `E`-valued function and the `F`-valued vector measure `μ` with linear
paring `B : E →L[ℝ] F →L[ℝ] G` . This is set to be `0` if `G` is not complete or if `f` is not
integrable with respect to `(μ.transpose B).variation`. Notation `∫ᵛ x, f x ∂[B; μ]`.

When `μ` is `G`-valued, to get the integral in `G` of a real-valued function, take
`B = ContinousLinearMap.lsmul ℝ ℝ`. Notation `∫ᵛ x, f x ∂•μ`.
When `μ` is a signed measure, to get the integral in `G` of a `G`-valued function, take
`B = (ContinousLinearMap.lsmul ℝ ℝ).flip`. Notation `∫ᵛ x, f x ∂<•μ`.
 -/
MeasureTheory.VectorMeasure.integral : {X : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      {G : Type u_6} →
        {mX : MeasurableSpace X} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NormedSpace ℝ F] →
                  [inst_4 : NormedAddCommGroup G] →
                    [inst_5 : NormedSpace ℝ G] → MeasureTheory.VectorMeasure X F → (X → E) → (E →L[ℝ] F →L[ℝ] G) → G
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.op_id_unop : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : Cᵒᵖ},
  (CategoryTheory.CategoryStruct.id (Opposite.unop X)).op = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.uliftFunctor_map : ∀ {x x_1 : AddCommGrpCat} (f : x ⟶ x_1),
  AddCommGrpCat.uliftFunctor.map f =
    AddCommGrpCat.ofHom
      (AddEquiv.ulift.symm.toAddMonoidHom.comp ((AddCommGrpCat.Hom.hom f).comp AddEquiv.ulift.toAddMonoidHom))
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- This is a simple version of the **Unfolding Trick**: Given a subgroup `Γ` of an
additive group `G`, the integral of a function `f` on `G` with respect to a right-invariant
measure `μ` is equal to the integral over the quotient `G ⧸ Γ` of the automorphization of `f`.  -/
QuotientAddGroup.integral_eq_integral_automorphize : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] {E : Type u_2}
      [inst_8 : NormedAddCommGroup E] [inst_9 : NormedSpace ℝ E] [μ.IsAddRightInvariant] {f : G → E},
      MeasureTheory.Integrable f μ →
        MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f)
            (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) →
          ∫ (x : G), f x ∂μ =
            ∫ (x : G ⧸ Γ),
              QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)
-- Mathlib.Tactic.Simps.NotationClass
/-- Data needed to generate automatic projections. This data is associated to a name of a projection
in a structure that must be used to trigger the search.  -/
Simps.AutomaticProjectionData : Type
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.of_equivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J']
  (e : J ≌ J') [P.IsClosedUnderColimitsOfShape J], P.IsClosedUnderColimitsOfShape J'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.abs_iterate_derivative_T_real_le : ∀ (n : ℤ) (k : ℕ) {x : ℝ},
  |x| ≤ 1 →
    |Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T ℝ n))| ≤
      Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T ℝ n))
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.def : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b ↔ ∃ n, ¬a ^ (n + 1) ∣ b
-- Lean.Meta.Match.NamedPatterns
Lean.Meta.Match.isNamedPattern? : Lean.Expr → Option Lean.Expr
-- Mathlib.Algebra.Star.Unitary
commute_unitary_self_star : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {u : R}, u ∈ unitary R → Commute u (star u)