mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.eq_of_encode_eq : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  (x y : α), HasModel.encode✝ x = HasModel.encode✝ y → x = y
-- Mathlib.Tactic.Translate.Core
/-- Get the translation name for the given name.  -/
Mathlib.Tactic.Translate.findTranslationName? : Lean.Environment → Mathlib.Tactic.Translate.TranslateData → Lean.Name → Option Lean.Name
-- Mathlib.Logic.Denumerable
/-- All denumerable types are equivalent.  -/
Denumerable.equiv₂ : (α : Type u_3) → (β : Type u_4) → [Denumerable α] → [Denumerable β] → α ≃ β
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaMonObjObjEquiv_symm_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Mon C} {Y Y' : C} (g : Y' ⟶ Y)
  (f : Y ⟶ M.X),
  CategoryTheory.shrinkYonedaMonObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g f) =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaMon.{w, v, u}.obj M).map g.op))
      (CategoryTheory.shrinkYonedaMonObjObjEquiv.symm f)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- The left action of a map `f : c ⟶ c'` in `C` on an object `d` in `D`.
If we are to consider the action as a functor `Α : C ⥤ D ⥤ D`,
this is `(Α.map f).app d`. This is denoted `f ⊵ₗ d`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft : {C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct C D] →
            {c c' : C} →
              (c ⟶ c') →
                (d : D) →
                  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d ⟶
                    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d
-- Mathlib.Data.Finset.Sups
Finset.union_mem_sups : ∀ {α : Type u_2} [inst : DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s t : Finset α}, s ∈ 𝒜 → t ∈ ℬ → s ∪ t ∈ 𝒜 ⊻ ℬ
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.val_J : ↑UpperHalfPlane.J = !![-1, 0; 0, 1]
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfMkEqMk_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
  (h : CategoryTheory.Subobject.mk f = CategoryTheory.Subobject.mk g),
  (CategoryTheory.Subobject.isoOfMkEqMk f g h).inv = CategoryTheory.Subobject.ofMkLEMk g f ⋯
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_coe_proj : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {x : B}
  {y : F} (e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj), x ∈ e'.baseSet → (↑e'.symm (x, y)).proj = x
-- Mathlib.Algebra.Category.Grp.Basic
/-- Turn a morphism in `CommGrpCat` back into a `MonoidHom`.  -/
CommGrpCat.Hom.hom : {X Y : CommGrpCat} → X.Hom Y → ↑X →* ↑Y
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.toEquiv_uniformEquiv : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → UniformSpace (β i)],
  (PiLp.uniformEquiv p β).toEquiv = WithLp.equiv p ((i : ι) → β i)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_arrow' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv
      (CategoryTheory.Limits.kernelSubobject f).arrow =
    CategoryTheory.Limits.kernel.ι f
-- Lean.Meta.Tactic.Cases
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.Cases.elimAuxIndices : Lean.Meta.GeneralizeIndicesSubgoal → Array Lean.Meta.CasesSubgoal → Lean.MetaM (Array Lean.Meta.CasesSubgoal)
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.workerExited : Lean.JsonRpc.ErrorCode
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel : (α : Type u) →
  [LE α] →
    [LT α] →
      (β : outParam (Type v)) →
        [inst : LE β] →
          [inst_1 : LT β] →
            [inst_2 : Std.PRange.UpwardEnumerable β] →
              [Std.PRange.LawfulUpwardEnumerable β] →
                [Std.PRange.LawfulUpwardEnumerableLE β] → [Std.PRange.LawfulUpwardEnumerableLT β] → Type (max u v)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- Return the finite place defined by a maximal ideal `v`.  -/
NumberField.FinitePlace.mk : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) → NumberField.FinitePlace K
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.Ioo_min_max : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioo (min a b) (max a b) = Set.uIoo a b
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_pos_iff : ∀ {k n : ℕ}, 0 < (ArithmeticFunction.sigma k) n ↔ 0 < n
-- Mathlib.Analysis.MeanInequalities
/-- For `1 ≤ p`, the `p`-th power of the sum of `f i` is bounded above by a constant times the
sum of the `p`-th powers of `f i`. Version for sums over finite sets, with `ℝ`-valued functions.  -/
Real.rpow_sum_le_const_mul_sum_rpow : ∀ {ι : Type u} (s : Finset ι) (f : ι → ℝ) {p : ℝ}, 1 ≤ p → (∑ i ∈ s, |f i|) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, |f i| ^ p
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- A subset `v` of a null-set `w` has zero measure if `w` is a subset of a negative set `u`.  -/
MeasureTheory.SignedMeasure.subset_negative_null_set : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v w : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasurableSet w →
        MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u →
          s w = 0 → w ⊆ u → v ⊆ w → s v = 0
-- Init.Grind.Lemmas
Lean.Grind.rfl_true : true = true
-- Init.Data.List.MapIdx
_private.Init.Data.List.MapIdx.0.List.mapFinIdx.go.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (as : List α)
  (motive : (x : List α) → (x_1 : Array β) → x.length + x_1.size = as.length → Sort u_3) (a : α) (as_1 : List α)
  (acc : Array β) (h : (a :: as_1).length + acc.size = as.length)
  (h_1 : (acc : Array β) → (h : [].length + acc.size = as.length) → motive [] acc h)
  (h_2 :
    (a : α) →
      (as_2 : List α) → (acc : Array β) → (h : (a :: as_2).length + acc.size = as.length) → motive (a :: as_2) acc h),
  (match a :: as_1, acc, h with
    | [], acc, h => h_1 acc h
    | a :: as_2, acc, h => h_2 a as_2 acc h) =
    h_2 a as_1 acc h
-- Init.Data.Int.DivMod.Lemmas
Int.add_mul_bmod_self_left : ∀ (a : ℤ) (b : ℕ) (c : ℤ), (a + ↑b * c).bmod b = a.bmod b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMinEntry!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)], t₁.Equiv t₂ → Std.DTreeMap.Const.minEntry! t₁ = Std.DTreeMap.Const.minEntry! t₂
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.run : {α : Type} → ℕ → Lean.Meta.Grind.Arith.Linear.LinearM α → Lean.Meta.Grind.GoalM α
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `J` is `u`-small, the forgetful functor from `AddMonCat.{u}` preserves limits
of shape `J`.  -/
AddMonCat.forget_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddMonCat)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.Polynomial.isRoot_cos_pi_div_five : (4 • Polynomial.X ^ 2 - 2 • Polynomial.X - Polynomial.C 1).IsRoot (Real.cos (Real.pi / 5))
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.widthInfty_pos : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic], 0 < 𝒢.widthInfty
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iSup_nonneg_of_nonnegHomClass : ∀ {ι : Type u_2} {F : Type u_3} {α : Type u_4} [inst : FunLike F α ℝ] [NonnegHomClass F α ℝ] (f : F) (g : ι → α),
  0 ≤ ⨆ i, f (g i)
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring module is an additive group, together with an additive action of a
Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms.
(For representations of Lie *algebras* see `LieModule`.)  -/
LieRingModule : (L : Type v) → (M : Type w) → [LieRing L] → [AddCommGroup M] → Type (max v w)
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanIso_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {f : α → β} {n : ℕ},
  IsAddFreimanIso n ∅ ∅ f
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods.pre : Lean.Meta.Sym.DSimp.Methods → Lean.Meta.Sym.DSimp.DSimproc
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.Simps.coe.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : LowerSet α), LowerSet.Simps.coe s = ↑s
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra : ∀ {R : Type u} [inst : CommRing R] {J : Type v} [inst_1 : CategoryTheory.Category.{t, v} J]
  (F : CategoryTheory.Functor J (AlgCat R)) [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections],
  Small.{w, max v w} ↥(AlgCat.sectionsSubalgebra F)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.cons : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  coef.Sorted →
    tl.leadingExp < ↑exp →
      tl.Sorted → (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl).Sorted
-- Mathlib.Algebra.Polynomial.Bivariate
/-- A constant viewed as a polynomial in two variables.  -/
Polynomial.CC : {R : Type u_1} → [inst : Semiring R] → R → Polynomial (Polynomial R)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddMonoidHom.withTopMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N),
  ⇑f.withTopMap = WithTop.map ⇑f
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.mk_def_of_ne : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0),
  RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p ⟨q, ⋯⟩ }
-- Mathlib.Algebra.MvPolynomial.Eval
/-- `map f p` maps a polynomial `p` across a ring hom `f`  -/
MvPolynomial.map : {R : Type u} →
  {S₁ : Type v} →
    {σ : Type u_1} →
      [inst : CommSemiring R] → [inst_1 : CommSemiring S₁] → (R →+* S₁) → MvPolynomial σ R →+* MvPolynomial σ S₁
-- Mathlib.Data.PNat.Basic
PNat.recOn_succ : ∀ (n : ℕ+) {p : ℕ+ → Sort u_1} (one : p 1) (succ : (n : ℕ+) → p n → p (n + 1)),
  (n + 1).recOn one succ = succ n (n.recOn one succ)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.isSymm_def : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I : R →+* R}
  {B : M →ₛₗ[I] M →ₗ[R] R}, B.IsSymm ↔ ∀ (x y : M), I ((B x) y) = (B y) x
-- Mathlib.Algebra.Module.Torsion.Free
Module.IsTorsionFree.of_smul_eq_zero : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial R],
  (∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0) → Module.IsTorsionFree R M
-- Mathlib.RingTheory.HopkinsLevitzki
IsSemiprimaryRing.finite_of_isArtinian : ∀ (R₀ : Type u_1) (R : Type u_2) (M : Type u) [inst : Ring R₀] [inst_1 : Ring R] [inst_2 : Module R₀ R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R₀ M] [inst_5 : Module R M] [IsScalarTower R₀ R M] [IsSemiprimaryRing R]
  [inst_8 : IsScalarTower R₀ R R] [Module.Finite R₀ (R ⧸ Ring.jacobson R)] [IsArtinian R M], Module.Finite R₀ M
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_pow : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (n : ℕ)
  (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_pow._auto_1 →
    autoParam (p a) cfc_pow._auto_3 → cfc (fun x => f x ^ n) a = cfc f a ^ n
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.not_isTrivial_completeOn : ∀ {α : Type u_1} (f : Set α), ¬(Hypergraph.completeOn f).IsTrivial
-- Std.Time.Zoned.Database.TZdb
/-- Retrieves the timezone rules for the given timezone ID, re-reading `TZDIR` on each
call so that runtime changes are reflected immediately.
 -/
Std.Time.Database.TZdb.getZoneRules : Std.Time.Database.TZdb → String → IO Std.Time.TimeZone.ZoneRules
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.ext_iff : ∀ {x y : Std.Time.PlainDate}, x = y ↔ x.year = y.year ∧ x.month = y.month ∧ x.day = y.day
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.natDegree_derivative_le : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), (Polynomial.derivative p).natDegree ≤ p.natDegree - 1
-- Mathlib.LinearAlgebra.RootSystem.BaseExists
RootPairing.nonempty_base : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [inst : AddCommGroup M]
  [inst_1 : AddCommGroup N] [inst_2 : Field R] [CharZero R] [inst_4 : Module R M] [inst_5 : Module R N]
  (P : RootPairing ι R M N) [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced], Nonempty P.Base
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.mul_def : ∀ (α : Type u_2) (t₁ t₂ : FirstOrder.Language.ring.Term α), t₁ * t₂ = FirstOrder.Ring.mulFunc.apply₂ t₁ t₂
-- Mathlib.Algebra.Prime.Defs
Prime.dvd_of_dvd_pow : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ∀ {a : M} {n : ℕ}, p ∣ a ^ n → p ∣ a
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
/-- The identity functor as a morphism of localizers.  -/
CategoryTheory.LocalizerMorphism.id : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    (W₁ : CategoryTheory.MorphismProperty C₁) → CategoryTheory.LocalizerMorphism W₁ W₁
-- Mathlib.Algebra.Ring.Rat
Rat.num_div_den : ∀ (r : ℚ), ↑r.num / ↑r.den = r
-- Mathlib.Analysis.LocallyConvex.Basic
Absorbent.submodule_eq_top : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {V : Submodule 𝕜 E}, Absorbent 𝕜 ↑V → V = ⊤
-- Lean.Declaration
Lean.DefinitionVal.mk.inj : ∀ {toConstantVal : Lean.ConstantVal} {value : Lean.Expr} {hints : Lean.ReducibilityHints}
  {safety : Lean.DefinitionSafety} {all : List Lean.Name} {toConstantVal_1 : Lean.ConstantVal} {value_1 : Lean.Expr}
  {hints_1 : Lean.ReducibilityHints} {safety_1 : Lean.DefinitionSafety} {all_1 : List Lean.Name},
  { toConstantVal := toConstantVal, value := value, hints := hints, safety := safety, all := all } =
      { toConstantVal := toConstantVal_1, value := value_1, hints := hints_1, safety := safety_1, all := all_1 } →
    toConstantVal = toConstantVal_1 ∧ value = value_1 ∧ hints = hints_1 ∧ safety = safety_1 ∧ all = all_1
-- Mathlib.Data.Int.Order.Units
Int.units_div_eq_mul : ∀ (u₁ u₂ : ℤˣ), u₁ / u₂ = u₁ * u₂
-- Mathlib.Data.EReal.Operations
/-- See also `EReal.sub_le_of_le_add`.  -/
EReal.sub_le_of_le_add' : ∀ {a b c : EReal}, a ≤ b + c → a - b ≤ c
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
multipliable_subtype_iff_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {s : Set β},
  Multipliable (f ∘ Subtype.val) ↔ Multipliable (s.mulIndicator f)
-- Mathlib.Topology.Separation.Basic
isClosed_setOfPred_specializes : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X], IsClosed {p | p.1 ⤳ p.2}
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.ofHom_injective : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : AddGroup Y], Function.Injective fun f => AddGrpCat.ofHom f
-- Lean.Meta.Closure
Lean.Meta.Closure.ToProcessElement.fvarId : Lean.Meta.Closure.ToProcessElement → Lean.FVarId
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f).getKey? k = if k ∈ t then some k else none
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_coeff_eq_zero_of_basis : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ι' : Type u_6} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ι'] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ι'] [inst_9 : Module.Free R M] [inst_10 : Module.Finite R M] (b : Module.Basis ι R L)
  (b' : Module.Basis ι' R L) (k : ℕ), (φ.polyCharpoly b).coeff k = 0 → (φ.polyCharpoly b').coeff k = 0
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comp_of_comap_eq : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] {v : NumberField.InfinitePlace k}
  {w : NumberField.InfinitePlace K} {f : k →+* K}, w.comap f = v → ∀ (x : k), w (f x) = v x
-- Init.Data.Fin.Bitwise
Fin.shiftLeft_val : ∀ {n : ℕ} (a b : Fin n), ↑(a <<< b) = ↑a <<< ↑b % n
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodCongr_apply : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (e : M ≃+ N) (e' : M' ≃+ N'),
  ⇑(e.coprodCongr e') = ⇑(AddMonoid.Coprod.map ↑e ↑e')
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
isSimpleRing_isArtinianRing_iff : ∀ {R : Type u} [inst : Ring R], IsSimpleRing R ∧ IsArtinianRing R ↔ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose : ℤ →
  Lean.Grind.CommRing.Mon →
    Lean.Meta.Grind.Arith.CommRing.EqCnstr →
      ℤ → Lean.Grind.CommRing.Mon → Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which antivary together, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not antivary together. Stated by permuting the entries of `f`.  -/
Antivary.sum_mul_lt_sum_comp_perm_mul_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι],
  Antivary f g → (∑ i, f i * g i < ∑ i, f (σ i) * g i ↔ ¬Antivary (f ∘ ⇑σ) g)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.MatchesAt.exists_isLongestMatchAt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos → ∃ endPos, String.Slice.Pattern.Model.IsLongestMatchAt pat pos endPos
-- Init.Data.Nat.Bitwise.Basic
/-- Shifts the binary representation of a value right by the specified number of bits. Usually accessed
via the `>>>` operator.

Examples:
 * `4 >>> 2 = 1`
 * `8 >>> 2 = 2`
 * `8 >>> 3 = 1`
 * `0 >>> 3 = 0`
 * `0xf13a >>> 8 = 0xf1`
 -/
Nat.shiftRight : ℕ → ℕ → ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- Auxiliary definition for `CofibrantObject.HoCat.adj`.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject.comp
          HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution ≅
        CategoryTheory.Functor.id (HomotopicalAlgebra.BifibrantObject.HoCat C)
-- Mathlib.Data.Fin.Tuple.Sort
/-- `sort f` is the permutation that orders `Fin n` according to the order of the outputs of `f`.  -/
Tuple.sort : {n : ℕ} → {α : Type u_1} → [LinearOrder α] → (Fin n → α) → Equiv.Perm (Fin n)
-- Std.Time.DateTime.Timestamp
Std.Time.instReprTimestamp : Repr Std.Time.Timestamp
-- Init.Data.SInt.Basic
/-- The modulo operator for 64-bit signed integers, which computes the remainder when dividing one
integer by another with the T-rounding convention used by `Int64.div`. Usually accessed via the `%`
operator.

When the divisor is `0`, the result is the dividend rather than an error.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int64.mod 5 2 = 1`
* `Int64.mod 5 (-2) = 1`
* `Int64.mod (-5) 2 = (-1)`
* `Int64.mod (-5) (-2) = (-1)`
* `Int64.mod 4 2 = 0`
* `Int64.mod 4 (-2) = 0`
* `Int64.mod 4 0 = 4`
* `Int64.mod (-4) 0 = (-4)`
 -/
Int64.mod : Int64 → Int64 → Int64
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instLinearOrderedAddCommGroupWithTopOrderDualAdditive : {α : Type u_1} → [LinearOrderedCommGroupWithZero α] → LinearOrderedAddCommGroupWithTop (Additive α)ᵒᵈ
-- ProofWidgets.Component.Panel.Basic
ProofWidgets.PanelWidgetProps.mk : Lean.Lsp.Position →
  Array Lean.Widget.InteractiveGoal →
    Option Lean.Widget.InteractiveTermGoal → Array Lean.SubExpr.GoalsLocation → ProofWidgets.PanelWidgetProps
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- A matrix multiplied by its conjugate transpose is positive semidefinite  -/
Matrix.posSemidef_self_mul_conjTranspose : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype n] [Finite m] [StarOrderedRing R] (A : Matrix m n R), (A * A.conjTranspose).PosSemidef
-- Mathlib.Geometry.Manifold.Complex
/-- A holomorphic function on a compact complex manifold is locally constant.  -/
MDifferentiable.isLocallyConstant : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type u_2} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {H : Type u_3} [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless]
  {M : Type u_4} [inst_6 : TopologicalSpace M] [inst_7 : ChartedSpace H M] [IsManifold I 1 M] [CompactSpace M]
  {f : M → F}, MDiff f → IsLocallyConstant f
-- Mathlib.Algebra.Quaternion
Quaternion.self_mul_star : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a * star a = ↑(Quaternion.normSq a)
-- Mathlib.Order.WithBot
WithTop.coe_le_iff : ∀ {α : Type u_1} {b : α} [inst : LE α] {x : WithTop α}, ↑b ≤ x ↔ ∀ (a : α), x = ↑a → b ≤ a
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_inv : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : Inv G] (f : α → G), ↑f⁻¹ = (↑f)⁻¹
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.Φ_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [Nontrivial R] (n : ℤ), W.Φ n ≠ 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.contains k = t.contains k'
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The property that the pentagon relation is satisfied by four objects
in a category equipped with a `MonoidalCategoryStruct`.  -/
CategoryTheory.MonoidalCategory.Pentagon : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategoryStruct C] → C → C → C → C → Prop
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_discard' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  (ProbabilityTheory.Kernel.discard β).comp κ =
    { toFun := fun a => (κ a) Set.univ • MeasureTheory.Measure.dirac PUnit.unit, measurable' := ⋯ }