mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.LibrarySuggestions.Basic
/-- Optional flag associated with the suggestion, e.g. "←" or "=",
if the premise selection algorithm is aware of the tactic consuming the results,
and wants to suggest modifiers for this suggestion.
E.g. this supports calling `simp` in the reverse direction,
or telling `grind` or `aesop` to use the theorem in a particular way.
 -/
Lean.LibrarySuggestions.Suggestion.flag : Lean.LibrarySuggestions.Suggestion → Option String
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.essSurj_map₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  [F.EssSurj] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β],
  (CategoryTheory.CostructuredArrow.map₂ α β).EssSurj
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblY_of_Y_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    P 2 ≠ 0 →
      Q 2 ≠ 0 →
        P 0 * Q 2 = Q 0 * P 2 →
          P 1 * Q 2 = Q 1 * P 2 →
            P 1 * Q 2 = W'.negY Q * P 2 → W'.dblY P * P 2 ^ 2 = (MvPolynomial.eval P) W'.polynomialX ^ 3
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- (Impl) A preliminary definition to avoid timeouts.  -/
CategoryTheory.Over.ConstructProducts.conesEquivInverse : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (B : C) →
      {J : Type w} →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) →
          CategoryTheory.Functor (CategoryTheory.Limits.Cone F)
            (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F))
-- Mathlib.Data.Nat.Totient
/-- A characterisation of `Nat.totient` that avoids `Finset`.  -/
Nat.totient_eq_card_lt_and_coprime : ∀ (n : ℕ), n.totient = Nat.card ↑{m | m < n ∧ n.Coprime m}
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.uniformSpace : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_4} →
            {F : Type u_5} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module 𝕜₂ F] →
                      [inst_6 : TopologicalSpace E] →
                        [inst_7 : UniformSpace F] → [IsUniformAddGroup F] → UniformSpace (E →SL[σ] F)
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.SchurZassenhausInduction.step4 : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index →
    (∀ (H : Subgroup G), ¬N.IsComplement' H) → ∀ [Finite G], Nat.Prime (Nat.card ↥N).minFac
-- Mathlib.Algebra.Group.TypeTags.Basic
toMul_zsmul : ∀ {α : Type u} [inst : DivInvMonoid α] (z : ℤ) (a : Additive α), Additive.toMul (z • a) = Additive.toMul a ^ z
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.toZFSet_rank_eq : ∀ {x : ZFSet.{u_1}}, x.IsOrdinal → x.rank.toZFSet = x
-- Mathlib.Algebra.Order.Field.Basic
div_lt_one_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b < 0 → (a / b < 1 ↔ b < a)
-- Aesop.Search.Expansion
Aesop.withRuleTraceNode : {Q : Type} →
  [inst : Aesop.Queue Q] → {α : Type} → Aesop.RuleName → (α → String) → String → Aesop.SearchM Q α → Aesop.SearchM Q α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.comap_supr : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] {ι : Sort u_8} (f : P₁ →ᵃ[k] P₂) (s : ι → AffineSubspace k P₂),
  AffineSubspace.comap f (iInf s) = ⨅ i, AffineSubspace.comap f (s i)
-- Mathlib.RingTheory.HahnSeries.HEval
PowerSeries.coeff_heval : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) (f : PowerSeries R) (g : Γ),
  ((PowerSeries.heval x) f).coeff g = ∑ᶠ (n : ℕ), ((HahnSeries.SummableFamily.powerSeriesFamily x f).coeff g) n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.fstKernelFork_ι : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y), CategoryTheory.Limits.Fork.ι c.fstKernelFork = c.inr
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iio_ofDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : αᵒᵈ),
  Finset.Iio (OrderDual.ofDual a) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioi a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Product of two affine equivalences. The map comes from `Equiv.prodCongr`  -/
AffineEquiv.prodCongr : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {P₃ : Type u_4} →
        {P₄ : Type u_5} →
          {V₁ : Type u_6} →
            {V₂ : Type u_7} →
              {V₃ : Type u_8} →
                {V₄ : Type u_9} →
                  [inst : Ring k] →
                    [inst_1 : AddCommGroup V₁] →
                      [inst_2 : AddCommGroup V₂] →
                        [inst_3 : AddCommGroup V₃] →
                          [inst_4 : AddCommGroup V₄] →
                            [inst_5 : Module k V₁] →
                              [inst_6 : Module k V₂] →
                                [inst_7 : Module k V₃] →
                                  [inst_8 : Module k V₄] →
                                    [inst_9 : AddTorsor V₁ P₁] →
                                      [inst_10 : AddTorsor V₂ P₂] →
                                        [inst_11 : AddTorsor V₃ P₃] →
                                          [inst_12 : AddTorsor V₄ P₄] →
                                            (P₁ ≃ᵃ[k] P₂) → (P₃ ≃ᵃ[k] P₄) → P₁ × P₃ ≃ᵃ[k] P₂ × P₄
-- Mathlib.Data.List.ReduceOption
List.reduceOption_eq_singleton_iff : ∀ {α : Type u_1} (l : List (Option α)) (a : α),
  l.reduceOption = [a] ↔ ∃ m n, l = List.replicate m none ++ some a :: List.replicate n none
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBySet_quotient_ideal_smul : ∀ {R : Type u_1} (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R),
  Module.IsTorsionBySet R (M ⧸ I • ⊤) ↑I
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_toInt16 : ∀ (x : Int8), x.toInt16.toNatClampNeg = x.toNatClampNeg
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- If we want to construct a finite relative CW complex we can add the conditions
`eventually_isEmpty_cell` and `finite_cell`, relax the condition `mapsTo` and remove the condition
`closed'`.  -/
Topology.RelCWComplex.mkFinite : {X : Type u} →
  [inst : TopologicalSpace X] →
    (C : Set X) →
      (D : outParam (Set X)) →
        (cell : ℕ → Type u) →
          (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) →
            (∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) →
              (∀ (n : ℕ), Finite (cell n)) →
                (∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) →
                  (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) →
                    (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) →
                      (Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) →
                        (∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D) →
                          (∀ (n : ℕ) (i : cell n),
                              Set.MapsTo (↑(map n i)) (Metric.sphere 0 1)
                                (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) →
                            IsClosed D →
                              D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C → Topology.RelCWComplex C D
-- Mathlib.RingTheory.Ideal.Over
Ideal.disjoint_primeCompl_of_liesOver : ∀ {A : Type u_2} [inst : CommSemiring A] {C : Type u_4} [inst_1 : Semiring C] [inst_2 : Algebra A C] (𝔓 : Ideal C)
  (p : Ideal A) [inst_3 : p.IsPrime] [hPp : 𝔓.LiesOver p], Disjoint ↑(Algebra.algebraMapSubmonoid C p.primeCompl) ↑𝔓
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
returning `none` if no such element exists.
 -/
Std.TreeSet.Raw.getGT? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → Option α
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft_obj_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E],
  (CategoryTheory.Functor.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C) =
    CategoryTheory.Functor.id (CategoryTheory.Functor C E)
-- Init.Data.List.Attach
List.unattach_replicate : ∀ {α : Type u_1} {p : α → Prop} {n : ℕ} {x : { x // p x }}, (List.replicate n x).unattach = List.replicate n ↑x
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul_single_apply : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : Group G] (x : MonoidAlgebra R G) (r : R) (g h : G),
  (x * MonoidAlgebra.single g r).coeff h = x.coeff (h * g⁻¹) * r
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A set is contained in its `spanPoints`.  -/
subset_spanPoints : ∀ (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 : Set P), s ⊆ spanPoints k s
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.left_unitor_hom_apply : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X : (i : I) → C i} {i : I},
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom i =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X i)).hom
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.col_eq_prod : ∀ {μ : YoungDiagram} {j : ℕ}, μ.col j = Finset.range (μ.colLen j) ×ˢ {j}
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_strictMono : StrictMono ZFSet.vonNeumann
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.norm_symm : ∀ (x y : ℤ), ‖![x, y]‖ = ‖![y, x]‖
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.brecOn.eq : ∀ {α : Type u} {motive : RBTree.RBNode α → Sort u_1} (t : RBTree.RBNode α)
  (F_1 : (t : RBTree.RBNode α) → RBTree.RBNode.below t → motive t),
  RBTree.RBNode.brecOn t F_1 = F_1 t (RBTree.RBNode.brecOn.go t F_1).2
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.instPreservesColimitLocallyRingedSpaceForgetToLocallyRingedSpace : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J],
  CategoryTheory.Limits.PreservesColimit F AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted_one : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ), PowerSeries.IsRestricted c 1
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- A partition of `n` is a multiset of positive integers summing to `n`.  -/
Nat.Partition : ℕ → Type
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.closureAddCommMonoidOfComm.eq_1 : ∀ (M : Type u_1) [inst : AddMonoid M] {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a + b = b + a),
  AddSubmonoid.closureAddCommMonoidOfComm M hcomm = inferInstance
-- Aesop.Stats.Basic
Aesop.instInhabitedGoalStats : Inhabited Aesop.GoalStats
-- Mathlib.Data.Finset.Sigma
Finset.coe_sigma : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (t : (i : ι) → Finset (α i)),
  ↑(s.sigma t) = (↑s).sigma fun i => ↑(t i)
-- Mathlib.Algebra.GroupWithZero.Semiconj
SemiconjBy.inv_symm_left₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a x y : G₀}, SemiconjBy a x y → SemiconjBy a⁻¹ y x
-- Mathlib.Tactic.Widget.Conv
/-- Traverses into the binder type of a forall, let, or lambda.
Currently out of these three options `conv` only supports going into
the binder type of a forall, but in the future if `conv` gets support for
going into let or lambda binding types with different `conv` tactics we may add
additional arguments to specify whether the binder is a forall, let, or lambda.
Corresponds to the `conv` tactics `lhs` or `arg`.
 -/
Mathlib.Tactic.Conv.Path.type : Mathlib.Tactic.Conv.Path → Mathlib.Tactic.Conv.Path
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace : ∀ {L : Type u_2} [inst : LieRing L] {K : Type u_4} [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L),
  LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ α, ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ LieAlgebra.rootSpace H ⇑α
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- The ultrafilter lemma: Any proper filter is contained in an ultrafilter.  -/
Ultrafilter.exists_le : ∀ {α : Type u} (f : Filter α) [h : f.NeBot], ∃ u, ↑u ≤ f
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.All.imp : ∀ {α : Type u_1} {p q : α → Prop},
  (∀ {x : α}, p x → q x) → ∀ {t : RBTree.RBNode α}, RBTree.RBNode.All p t → RBTree.RBNode.All q t
-- Init.Data.UInt.Bitwise
UInt32.toUInt64_not : ∀ (a : UInt32), (~~~a).toUInt64 = ~~~a.toUInt64 % 4294967296
-- Init.Data.Array.Lemmas
Array.getElem?_modify : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {f : α → α} {j : ℕ},
  (xs.modify i f)[j]? = if i = j then Option.map f xs[j]? else xs[j]?
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonAppDefault : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.instNontrivialLocallyConstantIntOfNonempty : ∀ {α : Type u_1} [inst : TopologicalSpace α] [Nonempty α], Nontrivial (LocallyConstant α ℤ)
-- Mathlib.Algebra.Order.Algebra
algebraMap_lt_algebraMap : ∀ {α : Type u_1} {β : Type u_2} [inst : CommSemiring α] [inst_1 : PartialOrder α] [inst_2 : Semiring β]
  [inst_3 : PartialOrder β] [inst_4 : Algebra α β] [ZeroLEOneClass β] [Nontrivial β] [SMulPosStrictMono α β]
  [SMulPosReflectLT α β] {a₁ a₂ : α}, (algebraMap α β) a₁ < (algebraMap α β) a₂ ↔ a₁ < a₂
-- Mathlib.Data.Set.Prod
Set.pi_congr : ∀ {ι : Type u_1} {α : ι → Type u_2} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  s₁ = s₂ → (∀ i ∈ s₁, t₁ i = t₂ i) → s₁.pi t₁ = s₂.pi t₂
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.image_cast_int_Ico : ∀ (a b : ℕ), Nat.cast '' Set.Ico a b = Set.Ico ↑a ↑b
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ (f g : MvPowerSeries σ R), MvPowerSeries.subst a (f * g) = MvPowerSeries.subst a f * MvPowerSeries.subst a g
-- Mathlib.Algebra.Module.Presentation.Free
/-- If `relations : Relations A` involved no relation, then it has an obvious
solution in the module `relations.G →₀ A`.  -/
Module.Relations.solutionFinsupp : {A : Type u} →
  [inst : Ring A] → (relations : Module.Relations A) → [IsEmpty relations.R] → relations.Solution (relations.G →₀ A)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take_take : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ), (p.take n).take m = (p.take (min n m)).copy ⋯ ⋯
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lt_bsup_of_ne_bsup : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}},
  (∀ (i : Ordinal.{u}) (h : i < o), f i h ≠ o.bsup f) ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f
-- Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian
/-- In cartesian categories, every morphism is deterministic (preserves the comonoid structure).  -/
CategoryTheory.CartesianCopyDiscard.instDeterministic : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y), CategoryTheory.Deterministic f
-- Mathlib.Order.TransfiniteIteration
transfiniteIterate_bot : ∀ {I : Type u} [inst : SupSet I] (φ : I → I) {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : WellFoundedLT J] [inst_4 : OrderBot J] (i₀ : I), transfiniteIterate φ ⊥ i₀ = i₀
-- Mathlib.Data.SetLike.Fintype
SetLike.instFinite : ∀ {A : Type u_1} {B : Type u_2} [SetLike A B] [Finite B], Finite A
-- Init.Data.SInt.Bitwise
Int64.toBitVec_shiftLeft : ∀ (a b : Int64), (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 64
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.comp : Turing.ToPartrec.Code → Turing.ToPartrec.Cont → Turing.ToPartrec.Cont
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticAt.iterated_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} [CompleteSpace F],
  AnalyticAt 𝕜 f x → ∀ (n : ℕ), AnalyticAt 𝕜 (deriv^[n] f) x
-- Lean.Meta.CongrTheorems
/-- Auxiliary type for applying `mkCast` at `mkCongrSimpCore?`
 -/
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo : Type
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.instFunLike : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] → [inst_3 : SetLike τ B] → {𝒜 : ι → σ} → {ℬ : ι → τ} → FunLike (𝒜 →+*ᵍ ℬ) A B
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.natTrans_op : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (α : CategoryTheory.TwoSquare T L R B),
  α.op.natTrans = CategoryTheory.NatTrans.op α.natTrans
-- Mathlib.Algebra.Group.Pointwise.Set.Small
small_mul : ∀ {α : Type u_1} (s t : Set α) [inst : Mul α] [Small.{u, u_1} ↑s] [Small.{u, u_1} ↑t], Small.{u, u_1} ↑(s * t)
-- Mathlib.Topology.Separation.Hausdorff
t2_iff_ultrafilter : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  T2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ nhds x → ↑f ≤ nhds y → x = y
-- Mathlib.Order.Atoms
/-- **Alias** of `CompleteAtomicBooleanAlgebra.eq_setOfPred_le_sSup_and_isAtom`. -/
CompleteAtomicBooleanAlgebra.eq_setOf_le_sSup_and_isAtom : ∀ {α : Type u_4} [inst : CompleteAtomicBooleanAlgebra α] {S : Set α},
  (∀ a ∈ S, IsAtom a) → S = {a | a ≤ sSup S ∧ IsAtom a}
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.Monic.decidable : {R : Type u} → [inst : Semiring R] → {p : Polynomial R} → [DecidableEq R] → Decidable p.Monic
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.of_forall_mem_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁.Equiv t₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.union_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ ∪ t₂).Equiv (t₁ ∪ t₃)
-- Mathlib.Order.Hom.BoundedLattice
/-- The function preserves the top element. The preferred spelling is `map_top`.  -/
BoundedLatticeHom.map_top' : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (self : BoundedLatticeHom α β), self.toFun ⊤ = ⊤
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.multisetProd_map_one : ∀ {α : Type u_1} {n : ℕ} {f : α → ℕ} {s : Multiset α}, (∀ x ∈ s, f x ≡ 1 [MOD n]) → (Multiset.map f s).prod ≡ 1 [MOD n]
-- Mathlib.Data.Finset.Sum
Finset.toLeft_image_swap : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (Finset.image Sum.swap u).toLeft = u.toRight
-- Mathlib.AlgebraicGeometry.Over
/-- `X.CanonicallyOver S` is the typeclass containing the data of a structure morphism `X ↘ S : X ⟶ S`,
and that `S` is (uniquely) inferable from the structure of `X`.
 -/
AlgebraicGeometry.Scheme.CanonicallyOver : AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.congr : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g₁ g₂ : α → F}, f₁ =o[l] g₁ → (∀ (x : α), f₁ x = f₂ x) → (∀ (x : α), g₁ x = g₂ x) → f₂ =o[l] g₂
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.mk.injEq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (toNonUnitalAlgHom : A →ₙₐ[R] B)
  (map_star' : ∀ (a : A), toNonUnitalAlgHom.toFun (star a) = star (toNonUnitalAlgHom.toFun a))
  (toNonUnitalAlgHom_1 : A →ₙₐ[R] B)
  (map_star'_1 : ∀ (a : A), toNonUnitalAlgHom_1.toFun (star a) = star (toNonUnitalAlgHom_1.toFun a)),
  ({ toNonUnitalAlgHom := toNonUnitalAlgHom, map_star' := map_star' } =
      { toNonUnitalAlgHom := toNonUnitalAlgHom_1, map_star' := map_star'_1 }) =
    (toNonUnitalAlgHom = toNonUnitalAlgHom_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonReferenceParams : Lean.ToJson Lean.Lsp.ReferenceParams
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_eq_zero : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A} {x : ↥S}, ↑x = 0 ↔ x = 0
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.instDistribLattice : DistribLattice YoungDiagram
-- Mathlib.Topology.Algebra.Support
isCompact_range_of_mulSupport_subset_isCompact : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β} {K : Set α}
  [inst_2 : TopologicalSpace β], Continuous f → IsCompact K → Function.mulSupport f ⊆ K → IsCompact (Set.range f)
-- Mathlib.Analysis.Fourier.LpSpace
/-- The `𝓢'`-inverse Fourier transform and the `L2`-inverse Fourier transform coincide on `L2`.  -/
MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E] (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)),
  FourierTransformInv.fourierInv (MeasureTheory.Lp.toTemperedDistribution f) =
    MeasureTheory.Lp.toTemperedDistribution (FourierTransformInv.fourierInv f)