mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Types
/-- `congr` is the term `self` is congruent to.
We say `self` is the congruence class root if `isSameExpr congr self`.
This field is initialized to `self` even if `e` is not an application.
 -/
Lean.Meta.Grind.ENode.congr : Lean.Meta.Grind.ENode → Lean.Expr
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.pow_succ : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : Lean.Grind.Ring.OfSemiring.Q α) (n : ℕ),
  Lean.Grind.Ring.OfSemiring.npow a (n + 1) = Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.npow a n) a
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.named.inj : ∀ {name : Lean.Name} {type default : Lean.Expr} {name_1 : Lean.Name} {type_1 default_1 : Lean.Expr},
  Lean.Doc.ArgSpec.named✝ name type default = Lean.Doc.ArgSpec.named✝ name_1 type_1 default_1 →
    name = name_1 ∧ type = type_1 ∧ default = default_1
-- Mathlib.Data.Finsupp.Defs
/-- `Finsupp.mapRange` of an injective function is injective.  -/
Finsupp.mapRange_injective : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (e : M → N) (he₀ : e 0 = 0),
  Function.Injective e → Function.Injective (Finsupp.mapRange e he₀)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.trStmts.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) [inst : Fintype σ] (S : Finset Λ),
  Turing.TM1to0.trStmts M S = Turing.TM1.stmts M S ×ˢ Finset.univ
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsPlot.contDiff : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n : ℕ} [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace ℝ X]
  [Diffeology.IsContDiffCompatible X] {p : EuclideanSpace ℝ (Fin n) → X}, Diffeology.IsPlot p → ContDiff ℝ (↑⊤) p
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.continuousMapEquiv_symm_apply_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  [inst_3 : CompactSpace α] (f : CompactlySupportedContinuousMap α β) (a : α),
  (CompactlySupportedContinuousMap.continuousMapEquiv.symm f) a = f a
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instNeg : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Neg (DoubleCentralizer 𝕜 A)
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- The level for 2-morphisms.  -/
Mathlib.Tactic.Bicategory.Context.level₂ : Mathlib.Tactic.Bicategory.Context → Lean.Level
-- Mathlib.Tactic.Convert
Convert.CheapConfig.mk : Congr!.Config → Convert.CheapConfig
-- Lean.Data.Json.Basic
Lean.strLt : String → String → Bool
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Complex.isBigO_cpow_rpow : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℂ},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |(g x).im|) →
    (fun x => f x ^ g x) =O[l] fun x => ‖f x‖ ^ (g x).re
-- Mathlib.Order.RelIso.Set
Subrel.instAsymmSubtype : ∀ {α : Type u_1} (r : α → α → Prop) [Std.Asymm r] (p : α → Prop), Std.Asymm (Subrel r p)
-- Mathlib.Data.Seq.Computation
Computation.equiv_pure_of_mem : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s → s.Equiv (Computation.pure a)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atTop_basis_Ioi : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] [Nonempty α] [NoMaxOrder α],
  Filter.atTop.HasBasis (fun x => True) Set.Ioi
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instSMulℂ : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  {k : ℤ} → {α : Type u_1} → [inst : SMul α ℂ] → [IsScalarTower α ℂ ℂ] → [Γ.HasDetOne] → SMul α (ModularForm Γ k)
-- Lean.DocString.Parser
/-- Parses an inline that is self-delimiting (that is, with well-defined start and stop characters).
 -/
Lean.Doc.Parser.delimitedInline : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.Data.Nat.Factorization.Basic
/-- The only numbers with empty prime factorization are `0` and `1`  -/
Nat.factorization_eq_zero_iff' : ∀ (n : ℕ), n.factorization = 0 ↔ n = 0 ∨ n = 1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod'_δ_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C E) [inst_6 : F.OplaxMonoidal]
  [inst_7 : G.OplaxMonoidal] (X Y : C),
  (CategoryTheory.Functor.OplaxMonoidal.δ (F.prod' G) X Y).1 = CategoryTheory.Functor.OplaxMonoidal.δ F X Y
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Multiplicative.toAdd_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : Multiplicative α}, Multiplicative.toAdd a < Multiplicative.toAdd b ↔ a < b
-- Init.Data.Fin.Lemmas
Fin.coe_castSucc : ∀ {n : ℕ} (i : Fin n), ↑i.castSucc = ↑i
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A choice of a generator for Lüroth's theorem, see `Luroth.eq_adjoin_generator`.  -/
RatFunc.Luroth.generator : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → RatFunc K
-- Lean.Expr
Lean.Nat.mkInstMod : Lean.Expr
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.toLp_single : ∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] (i : ι)
  (a : β i), WithLp.toLp p (Pi.single i a) = PiLp.single p i a
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instNoZeroDivisors : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [NoZeroDivisors α], NoZeroDivisors αᵐᵒᵖ
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_toCloseds : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] (s : TopologicalSpace.NonemptyCompacts α),
  ↑s.toCloseds = ↑s
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- If `x` is not congruent to `a` modulo `p`, then `toIocDiv` is continuous at `x`.

In fact, it is locally near `x`, see `eventuallyEq_toIocDiv_nhds`.  -/
continuousAt_toIocDiv : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜},
  ¬x ≡ a [PMOD p] → ContinuousAt (toIocDiv hp a) x
-- Init.Data.Vector.Lemmas
Vector.map_congr_left : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {α_1 : Type u_2} {f g : α → α_1},
  (∀ a ∈ xs, f a = g a) → Vector.map f xs = Vector.map g xs
-- Mathlib.RingTheory.QuotSMulTop
QuotSMulTop.map_comp : ∀ {R : Type u_2} [inst : CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} {M'' : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] [inst_5 : AddCommGroup M'']
  [inst_6 : Module R M''] (g : M' →ₗ[R] M'') (f : M →ₗ[R] M'),
  (QuotSMulTop.map r) (g ∘ₗ f) = (QuotSMulTop.map r) g ∘ₗ (QuotSMulTop.map r) f
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.odd_orderOf_of_involutive : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F} [Finite G],
  MonoidHom.FixedPointFree ⇑φ → Function.Involutive ⇑φ → ∀ (g : G), Odd (orderOf g)
-- Mathlib.Order.Heyting.Basic
sdiff_sdiff_sdiff_le_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ (a \ c) ≤ c \ b
-- Mathlib.Analysis.Convex.Body
ConvexBody.coe_smul' : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V]
  [inst_3 : ContinuousSMul ℝ V] (c : NNReal) (K : ConvexBody V), ↑(c • K) = c • ↑K
-- Mathlib.Algebra.Star.StarRingHom
/-- Turn an element of a type `F` satisfying `NonUnitalStarRingHomClass F A B` into an actual
`NonUnitalStarRingHom`. This is declared as the default coercion from `F` to `A →⋆ₙ+ B`.  -/
NonUnitalStarRingHomClass.toNonUnitalStarRingHom : {F : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : NonUnitalNonAssocSemiring A] →
        [inst_1 : Star A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [inst_3 : Star B] →
              [inst_4 : FunLike F A B] →
                [inst_5 : NonUnitalRingHomClass F A B] → [NonUnitalStarRingHomClass F A B] → F → A →⋆ₙ+* B
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_le_ofNat : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} {n : ℕ}
  [inst_3 : n.AtLeastTwo], ↑p ≤ OfNat.ofNat n ↔ p ≤ OfNat.ofNat n
-- Mathlib.Algebra.Category.MonCat.Colimits
/-- The cocone over the proposed colimit monoid.  -/
MonCat.Colimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] → (F : CategoryTheory.Functor J MonCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.Indep.isBasis_setOfPred_insert_isBasis`. -/
Matroid.Indep.isBasis_setOf_insert_isBasis : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → M.IsBasis I {x | M.IsBasis I (insert x I)}
-- Mathlib.Data.Set.List
Set.range_list_getElem? : ∀ {α : Type u_1} (l : List α), (Set.range fun x => l[x]?) = insert none (some '' {x | x ∈ l})
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
IsUniformInducing.isUniformGroup : ∀ {G : Type u_1} {H : Type u_2} {hom : Type u_3} [inst : Group G] [inst_1 : Group H] [inst_2 : UniformSpace G]
  [inst_3 : UniformSpace H] [IsUniformGroup H] [inst_5 : FunLike hom G H] [MonoidHomClass hom G H] (f : hom),
  IsUniformInducing ⇑f → IsUniformGroup G
-- Mathlib.Order.SuccPred.Basic
Order.pred_wcovBy : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] (a : α), Order.pred a ⩿ a
-- Mathlib.MeasureTheory.Measure.OpenPos
IsOpen.measure_zero_iff_eq_empty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {U : Set X}, IsOpen U → (μ U = 0 ↔ U = ∅)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.hint.sizeOf_spec : sizeOf Lean.Lsp.DiagnosticSeverity.hint = 1
-- Init.Data.List.Attach
List.attach_filter : ∀ {α : Type u_1} {l : List α} (p : α → Bool),
  (List.filter p l).attach = List.filterMap (fun x => if w : p ↑x = true then some ⟨↑x, ⋯⟩ else none) l.attach
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piSplitLE_eq : ∀ {ι : Type u_6} {X : ι → Type u_8} {i : ι} [inst : PartialOrder ι] [inst_1 : DecidableEq ι]
  {f : InverseSystem.piLT X i × X i}, InverseSystem.piSplitLE f ⟨i, ⋯⟩ = f.2
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {Z_1 : C} (h : CategoryTheory.Limits.pushout g f ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g f) h
-- Lean.Meta.Tactic.SplitIf
/-- Return an `if-then-else` or `match-expr` to split.  -/
Lean.Meta.findSplit? : Lean.Expr →
  optParam Lean.Meta.SplitKind Lean.Meta.SplitKind.both → optParam Lean.ExprSet ∅ → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpen_image_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsOpen (OnePoint.some '' s) ↔ IsOpen s
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- A weaker version of `Basis.opNNNorm_le` that abstracts away the value of `C`.  -/
Module.Basis.exists_opNNNorm_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  {ι : Type u_1} [Finite ι] (v : Module.Basis ι 𝕜 E),
  ∃ C > 0, ∀ {u : E →L[𝕜] F} (M : NNReal), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_commonNeighbors_le_degree_right : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v w : V),
  Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree w
-- Std.Http.Internal.IndexMultiMap
_private.Std.Http.Internal.IndexMultiMap.0.Std.Internal.IndexMultiMap.insert.match_1.eq_1 : ∀ (motive : Option (Array ℕ) → Sort u_1) (idxs : Array ℕ) (h_1 : (idxs : Array ℕ) → motive (some idxs))
  (h_2 : Unit → motive none),
  (match some idxs with
    | some idxs => h_1 idxs
    | none => h_2 ()) =
    h_1 idxs
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.IsStableUnderSup.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C},
  (∀ {X : C} {R S : CategoryTheory.Presieve X}, R ∈ J.coverings X → S ∈ J.coverings X → R ⊔ S ∈ J.coverings X) →
    J.IsStableUnderSup
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.zero_mem_resolventSet_of_unit : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : Aˣ),
  0 ∈ resolventSet R ↑a
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.Inv_divided_by_X_pow_order.congr_simp : ∀ {k : Type u_2} [inst : Field k] {f f_1 : PowerSeries k} (e_f : f = f_1) (hf : f ≠ 0) (a a_1 : Unit →₀ ℕ),
  a = a_1 → PowerSeries.Inv_divided_by_X_pow_order hf a = PowerSeries.Inv_divided_by_X_pow_order ⋯ a_1
-- Plausible.Sampleable
/-- `e` is a type to sample from, this can either be a type that implements `SampleableExt` or `Gen α`
directly. For this return:
- the universe level of the `Type u` that the relevant type to sample lives in.
- the actual type `α` to sample from
- a `Repr α` instance
- a `Gen α` generator to run in order to sample
 -/
_private.Plausible.Sampleable.0.Plausible.mkGenerator : Lean.Expr → Lean.MetaM (Lean.Level × Lean.Expr × Lean.Expr × Lean.Expr)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_sub_left : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Sub β] [MeasurableSub₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.IndepFun (f i - f j) (f k) μ
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.max? = none
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) The key property defining the map `λ : TL ⟶ L`.  -/
CategoryTheory.Monad.ForgetCreatesColimits.commuting : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] (j : J),
  CategoryTheory.CategoryStruct.comp (T.map (c.ι.app j)) (CategoryTheory.Monad.ForgetCreatesColimits.lambda c t) =
    CategoryTheory.CategoryStruct.comp (D.obj j).a (c.ι.app j)
-- Std.Http.Server.Config
/-- Maximum time (in milliseconds) allowed to receive the complete request headers after the first
byte of a new request arrives. This prevents Slowloris-style attacks where a client sends bytes
at a slow rate to hold a connection slot open without completing a request. Once a request starts,
each individual read must complete within this window. Default: 5 seconds.
 -/
Std.Http.Config.headerTimeout : Std.Http.Config → Std.Time.Millisecond.Offset
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (s : σ), ↑(MvPolynomial.X s) = MvPowerSeries.X s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The vector span of a union of sets with a common point is the sup of their vector spans.  -/
AffineSubspace.vectorSpan_union_of_mem_of_mem : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : Set P} {p : P},
  p ∈ s₁ → p ∈ s₂ → vectorSpan k (s₁ ∪ s₂) = vectorSpan k s₁ ⊔ vectorSpan k s₂
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.to_distribMulActionHom_injective : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] {f g : A →ₛₙₐ[φ] B}, ↑f = ↑g → f = g
-- Init.Data.UInt.Bitwise
UInt8.toUInt16_shiftRight : ∀ (a b : UInt8), (a >>> b).toUInt16 = a.toUInt16 >>> (b.toUInt16 % 8)
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` respects isomorphisms, to check `P` holds locally for `f : R →+* S`, it suffices
to check `P` holds on a standard open cover.  -/
RingHom.locally_of_exists : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {R S : Type u}
  [inst : CommRing R] [inst_1 : CommRing S],
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ (f : R →+* S) {ι : Type u_1} (s : ι → S),
      Ideal.span (Set.range s) = ⊤ →
        ∀ (Sₜ : ι → Type u) [inst_2 : (i : ι) → CommRing (Sₜ i)] [inst_3 : (i : ι) → Algebra S (Sₜ i)]
          [∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)],
          (∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)) → RingHom.Locally (fun {R S} [CommRing R] [CommRing S] => P) f
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.coe_mul : ∀ {𝕜 : Type u_1} [inst : SeminormedRing 𝕜] [inst_1 : NormMulClass 𝕜] [inst_2 : NormOneClass 𝕜]
  (x y : ↑(Metric.sphere 0 1)), ↑(x * y) = ↑x * ↑y
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
/-- The recursion `hermite (n+1) = (x - d/dx) (hermite n)`  -/
Polynomial.hermite_succ : ∀ (n : ℕ),
  Polynomial.hermite (n + 1) = Polynomial.X * Polynomial.hermite n - Polynomial.derivative (Polynomial.hermite n)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instAddCommMonoid : {k : Type u_1} → {G : Type u_2} → [inst : AddCommMonoid k] → AddCommMonoid (SkewMonoidAlgebra k G)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.mapRingHom_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} [inst_1 : Semiring Y] [inst_2 : Semiring Z]
  (f : Y →+* Z) (g : LocallyConstant X Y) (a : X), ((LocallyConstant.mapRingHom f) g) a = f (g a)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.numVars : Lean.Elab.Command.AddAndFinalizeContext✝ → ℕ
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.below.sq_add : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {motive : (a : R) → IsSumSq a → Prop} (a : R) {s : R}
  (hs : IsSumSq s), IsSumSq.below hs → motive s hs → IsSumSq.below ⋯
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- If the singleton `{x}` has non-zero mass for `ρ.fst`, then for all `s : Set Ω`,
`ρ.condKernel x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)` .  -/
MeasureTheory.Measure.condKernel_apply_of_ne_zero : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [inst_2 : MeasureTheory.IsFiniteMeasure ρ]
  [MeasurableSingletonClass α] {x : α}, ρ.fst {x} ≠ 0 → ∀ (s : Set Ω), (ρ.condKernel x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.sub_notMem_range_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [CharZero R] {i j : ι}, i ∈ b.support → j ∈ b.support → P.root i - P.root j ∉ Set.range ⇑P.root
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorem.mk.injEq : ∀ (theoremName funName : Lean.Name) (hypothesesPos : Array ℕ) (priority : ℕ) (theoremName_1 funName_1 : Lean.Name)
  (hypothesesPos_1 : Array ℕ) (priority_1 : ℕ),
  ({ theoremName := theoremName, funName := funName, hypothesesPos := hypothesesPos, priority := priority } =
      { theoremName := theoremName_1, funName := funName_1, hypothesesPos := hypothesesPos_1,
        priority := priority_1 }) =
    (theoremName = theoremName_1 ∧ funName = funName_1 ∧ hypothesesPos = hypothesesPos_1 ∧ priority = priority_1)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_succ_right_eq_append : ∀ {m n : ℕ}, m < n → (m<...n + 1).toList = (m<...n).toList ++ [n]
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (↑(m.insertMany l)).get? k = m.get? k
-- Lean.Meta.Tactic.Simp.Types
/-- For `pre` procedures, it returns the result without visiting any subexpressions.

For `post` procedures, it returns the result.
 -/
Lean.Meta.Simp.Step.done : Lean.Meta.Simp.Result → Lean.Meta.Simp.Step
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformLeft_neg : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommGroup α] (e : α) (x : Finset α × Finset α),
  Finset.addETransformLeft (-e) x = (Finset.addETransformRight e x.swap).swap
-- Mathlib.NumberTheory.LSeries.Convolution
LSeries.convolution_map_zero : ∀ {R : Type u_1} [inst : Semiring R] (f g : ℕ → R), LSeries.convolution f g 0 = 0
-- Mathlib.Analysis.Calculus.Deriv.Slope
hasDerivAt_iff_tendsto_slope_left_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [inst_3 : LinearOrder 𝕜],
  HasDerivAt f f' x ↔
    Filter.Tendsto (slope f x) (nhdsWithin x (Set.Iio x)) (nhds f') ∧
      Filter.Tendsto (slope f x) (nhdsWithin x (Set.Ioi x)) (nhds f')
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.snd_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (q : G.Walk v w) (hadj : G.Adj u v),
  (SimpleGraph.Walk.cons hadj q).snd = v
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ), MvPolynomial.coeff m 0 = 0
-- Mathlib.Topology.Compactness.Compact
IsCompact.finite : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → IsDiscrete s → s.Finite
-- Mathlib.Topology.EMetricSpace.Defs
WeakPseudoEMetricSpace.edist_triangle : ∀ {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x y z : α), edist x z ≤ edist x y + edist y z
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `f ◁ η` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.MkEval.mkEvalWhiskerLeft : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEval m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₂ →
        Mathlib.Tactic.BicategoryLike.NormalExpr →
          Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.snd.eq_1 : ∀ {R : Type u} {M : Type v} (x : TrivSqZeroExt R M), x.snd = x.2
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.isMultiplicative_moebius : ArithmeticFunction.moebius.IsMultiplicative
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_union_sdiff_cancel : ∀ {α : Type u_1} {s t u : Set α}, t ⊆ s → u ⊆ t → s \ t ∪ t \ u = s \ u