mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.mk : {R : Type u_7} →
  {S : Type u_8} →
    [inst : Mul R] →
      [inst_1 : Mul S] →
        [inst_2 : Add R] →
          [inst_3 : Add S] →
            (toEquiv : R ≃ S) →
              (∀ (x y : R), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y) →
                (∀ (x y : R), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y) → R ≃+* S
-- Mathlib.GroupTheory.GroupAction.Basic
Finite.of_finite_addAction_orbitRel_quotient : ∀ (G : Type u_1) (α : Type u_2) [inst : AddGroup G] [inst_1 : AddAction G α] [Finite G]
  [Finite (AddAction.orbitRel.Quotient G α)], Finite α
-- Batteries.Tactic.Lint.Basic
/-- Defines the `env_linter` extension for adding a linter to the default set.  -/
Batteries.Tactic.Lint.batteriesLinterExt : Lean.SimplePersistentEnvExtension (Lean.Name × Bool) (Lean.NameMap (Lean.Name × Bool))
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.BitVecValue.n : Lean.Meta.Sym.BitVecValue → ℕ
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.descFunLift.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (s : CategoryTheory.Limits.Cocone F) (j : J) (x_1 : ↑(F.obj j)),
  CommRingCat.Colimits.descFunLift F s (CommRingCat.Colimits.Prequotient.of j x_1) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x_1
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.coe_zero : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : Zero R], ⇑0 = 0
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.add_eq_eval₃ : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {a₁ : R × M}
  (a₂ : R × M) {l₁ l₂ l : Mathlib.Tactic.Module.NF R M},
  (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval → (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Topology.Basic.0.TopModuleCat.Hom.ofHom'.injEq : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y : TopModuleCat R}
  (hom' hom'_1 : ↑X.toModuleCat →L[R] ↑Y.toModuleCat), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.add_divMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x y : MvPolynomial σ R) (s : σ →₀ ℕ),
  (x + y).divMonomial s = x.divMonomial s + y.divMonomial s
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- Change the index category for `ObjectProperty.ColimitOfShape`.  -/
CategoryTheory.ObjectProperty.ColimitOfShape.reindex : {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'] →
              {X : C} → P.ColimitOfShape J X → (G : CategoryTheory.Functor J' J) → [G.Final] → P.ColimitOfShape J' X
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instIsRightAdjointModuleCatIndiscrete : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R], (TopModuleCat.indiscrete R).IsRightAdjoint
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The family of arrows of the discrete groupoid  -/
CategoryTheory.Subgroupoid.Discrete.Arrows : {C : Type u} → [inst : CategoryTheory.Groupoid C] → (c d : C) → (c ⟶ d) → Prop
-- Lean.Parser.Extra
Lean.ppHardSpace.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.BigOperators.Fin
_private.Mathlib.Algebra.BigOperators.Fin.0.List.alternatingSum.match_1.splitter : {G : Type u_1} →
  (motive : List G → Sort u_2) →
    (x : List G) →
      (Unit → motive []) → ((g : G) → motive [g]) → ((g h : G) → (t : List G) → motive (g :: h :: t)) → motive x
-- Mathlib.Order.Comparable
antisymmRel_compl : ∀ {α : Type u_1} (r : α → α → Prop), AntisymmRel rᶜ = IncompRel r
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- The projection map Π i, X i → X i induces a map π(Π i, X i) ⟶ π(X i).
 -/
FundamentalGroupoidFunctor.proj : {I : Type u} →
  (X : I → TopCat) →
    (i : I) →
      CategoryTheory.Functor ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of ((i : I) → ↑(X i))))
        ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))
-- Mathlib.Analysis.Normed.Group.Basic
norm_nonneg : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), 0 ≤ ‖a‖
-- Lean.Data.Lsp.Internal
/-- Start line of range.  -/
Lean.Lsp.DeclInfo.rangeStartPosLine : Lean.Lsp.DeclInfo → ℕ
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_or : ∀ {σs : List (Type u)} {φ₁ φ₂ : Prop}, ⌜φ₁⌝ ∨ ⌜φ₂⌝ ⊣⊢ₛ ⌜φ₁ ∨ φ₂⌝
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_surjective_iff_injective : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {A' : Type u_1} [inst_2 : AddCommGroup A']
  [inst_3 : Module R A] [inst_4 : Module R A'] {f : A →ₗ[R] A'},
  Function.Surjective ⇑(CharacterModule.dual f) ↔ Function.Injective ⇑f
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.zsmul_lt_zsmul_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.IntModule M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] (k : ℤ) {a b : M}, a < b → (k • a < k • b ↔ 0 < k)
-- Mathlib.Order.Cover
WCovBy.covBy_of_not_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → ¬b ≤ a → a ⋖ b
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings
/-- The functor `PresheafOfModules.restrictScalars α` induces bijections on
morphisms if `α` is locally surjective and the target presheaf is a sheaf.  -/
PresheafOfModules.restrictHomEquivOfIsLocallySurjective : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} →
        (α : R ⟶ R') →
          {M₁ M₂ : PresheafOfModules R'} →
            CategoryTheory.Presheaf.IsSheaf J M₂.presheaf →
              [CategoryTheory.Presheaf.IsLocallySurjective J α] →
                (M₁ ⟶ M₂) ≃
                  ((PresheafOfModules.restrictScalars α).obj M₁ ⟶ (PresheafOfModules.restrictScalars α).obj M₂)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instLE : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [LE Y] → [inst_2 : Zero Y] → LE (Function.locallyFinsuppWithin U Y)
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.mapsto_domChart_source_codChart_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), Set.MapsTo f h.domChart.source h.codChart.source
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeAux_comp : ∀ {B : Type u} [inst : Quiver B] {a : B} {b c d : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b) (f : b ⟶ c)
  (g : c ⟶ d),
  CategoryTheory.FreeBicategory.normalizeAux p (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.FreeBicategory.normalizeAux (CategoryTheory.FreeBicategory.normalizeAux p f) g
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.contMDiffOn_invFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (self : PartialDiffeomorph I J M N n),
  ContMDiffOn J I n self.invFun self.target
-- Mathlib.Data.List.Sort
RelIso.pairwise_listMap : ∀ {α : Type u_1} {β : Type u_2} {ra : α → α → Prop} {rb : β → β → Prop} (e : ra ≃r rb) {l : List α},
  List.Pairwise rb (List.map (⇑e) l) ↔ List.Pairwise ra l
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs_add : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (N : LieSubmodule R L M)
  [inst_6 : LieModule R L M] (k l : ℕ), LieSubmodule.ucs (k + l) N = LieSubmodule.ucs k (LieSubmodule.ucs l N)
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The modular discriminant `Δ(z) = η(z) ^ 24`, where `η` is the Dedekind eta function.  -/
ModularForm.discriminant : UpperHalfPlane → ℂ
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mdifferentiableAt_coordChangeL : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj} [inst_13 : MemTrivializationAtlas e]
  [inst_14 : MemTrivializationAtlas e'] [inst_15 : VectorBundle 𝕜 F E] [ContMDiffVectorBundle 1 F E IB] {x : B},
  x ∈ e.baseSet → x ∈ e'.baseSet → (MDiffAt fun b => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' b)) x
-- Mathlib.Computability.RegularExpressions
/-- `matches' P` provides a language which contains all strings that `P` matches.

Not named `matches` since that is a reserved word.
 -/
RegularExpression.matches' : {α : Type u_1} → RegularExpression α → Language α
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: if `a ≤ b` and `f' a ≤ m ≤ f' b`, then `f' c = m` for some
`c ∈ [a, b]`.  -/
exists_hasDerivWithinAt_eq_of_ge_of_le : ∀ {a b : ℝ} {f f' : ℝ → ℝ},
  a ≤ b →
    (∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
      ∀ {m : ℝ}, f' a ≤ m → m ≤ f' b → m ∈ f' '' Set.Icc a b
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.insert_eq_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {p : α}, insert p t = t.insert p
-- Mathlib.Data.Set.Finite.Basic
Finite.Set.finite_inter_of_right : ∀ {α : Type u} (s t : Set α) [Finite ↑t], Finite ↑(s ∩ t)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffWithinAt.add_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {u : Set M} {x₀ : M},
  ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u x₀ →
    ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) u x₀ →
      ContMDiffWithinAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (s + t) x⟩) u x₀
-- Mathlib.Lean.Meta.Basic
/-- `pureIsDefEq e₁ e₂` is short for `withNewMCtxDepth <| isDefEq e₁ e₂`.
Determines whether two expressions are definitionally equal to each other
when metavariables are not assignable.  -/
Lean.Meta.pureIsDefEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgEquiv.subalgebraMap_apply_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (x : ↑↑S.toAddSubmonoid),
  ↑((e.subalgebraMap S) x) = e ↑x
-- Mathlib.CategoryTheory.Action.Limits
Action.forget₂_additive : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.Preadditive V] {FV : V → V → Type u_3} {CV : V → Type u_4}
  [inst_3 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_4 : CategoryTheory.ConcreteCategory V FV],
  (CategoryTheory.forget₂ (Action V G) V).Additive
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_map : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (s : NonUnitalSubsemiring R),
  ↑(NonUnitalSubsemiring.map f s) = ⇑f '' ↑s
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.mkOfHomFunctors_toPrelaxFunctorStruct : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B → C)
  (F' : (a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)),
  (CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').toPrelaxFunctorStruct =
    CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F fun a b => (F' a b).toPrefunctor
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.eq : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.AEDisjoint μ s t → μ (s ∩ t) = 0
-- Lean.Level
Lean.Level.substParams : Lean.Level → (Lean.Name → Option Lean.Level) → Lean.Level
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- The base ring is a right identity for the tensor product of modules, up to linear equivalence.
 -/
TensorProduct.rid : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_5) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorProduct R M R ≃ₗ[R] M
-- Init.Data.BitVec.Basic
/-- Returns a bitvector of size `n` where all bits are `0`.  -/
BitVec.zero : (n : ℕ) → BitVec n
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `ComposableArrows C m ⥤ ComposableArrows C n` obtained by precomposition with
a functor `Fin (n + 1) ⥤ Fin (m + 1)`.  -/
CategoryTheory.ComposableArrows.whiskerLeftFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n m : ℕ} →
      CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1)) →
        CategoryTheory.Functor (CategoryTheory.ComposableArrows C m) (CategoryTheory.ComposableArrows C n)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The free tensor algebra over a direct sum of `R`-algebras, before
taking the quotient by the free product relation  -/
LinearAlgebra.FreeProduct.FreeTensorAlgebra : {I : Type u} →
  (R : Type v) →
    [inst : CommSemiring R] →
      (A : I → Type w) → [inst_1 : (i : I) → Semiring (A i)] → [(i : I) → Algebra R (A i)] → Type (max v w u)
-- Mathlib.Algebra.Category.Grp.Ulift
GrpCat.uliftFunctor_preservesLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J GrpCat.uliftFunctor
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.ker_le_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂} [inst_6 : RingHomSurjective τ₁₂] {p : Submodule R M}, f.ker ≤ p ↔ ∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑p
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) (a : ↥ℤ[ζ]),
  hζ.adjoinEquivRingOfIntegersOfPrimePow a = (IsIntegralClosure.lift ℤ (NumberField.RingOfIntegers K) K) a
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.iterFromIdx_equiv_iter_drop_toList : ∀ {n : ℕ} {α : Type w} {xs : Vector α n} {pos : ℕ}, (xs.iterFromIdx pos).Equiv (List.drop pos xs.toList).iter
-- Mathlib.Algebra.Order.Field.Basic
div_le_iff_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (b / c ≤ a ↔ a * c ≤ b)
-- Mathlib.Algebra.Group.Action.Units
IsAddUnit.neg_vadd : ∀ {α : Type u_5} [inst : AddMonoid α] {a : α} (h : IsAddUnit a), -h.addUnit +ᵥ a = 0
-- Lean.Widget.InteractiveCode
Lean.Widget.instToJsonDiffTag.toJson : Lean.Widget.DiffTag → Lean.Json
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (s : X ⟶ Y) (hs : W s),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso s hs).hom =
    (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map s
-- Lean.Parser.Term
Lean.Parser.Term.typeOf.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Complex.UpperHalfPlane.Exp
UpperHalfPlane.norm_exp_two_pi_I_lt_one : ∀ (τ : UpperHalfPlane), ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑τ)‖ < 1
-- Mathlib.Algebra.Regular.SMul
IsSMulRegular.mul_iff_right : ∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : SMul R M] [inst_1 : Mul R] [IsScalarTower R R M],
  IsSMulRegular M a → (IsSMulRegular M (a * b) ↔ IsSMulRegular M b)
-- Mathlib.Order.SuccPred.Basic
WithTop.succ_coe_of_isMax : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : (a : α) → Decidable (Order.succ a = a)]
  {a : α}, IsMax a → Order.succ ↑a = ⊤
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.mk.inj : ∀ {toGrp : GrpCat} {isFinite : Finite ↑toGrp} {toGrp_1 : GrpCat} {isFinite_1 : Finite ↑toGrp_1},
  { toGrp := toGrp, isFinite := isFinite } = { toGrp := toGrp_1, isFinite := isFinite_1 } → toGrp = toGrp_1
-- Mathlib.Algebra.Order.Group.PosPart
negPart_nonneg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] (a : α), 0 ≤ a⁻
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
_private.Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2.0.MeasureTheory.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.mem_find : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (x : X), x ∈ K (K.find x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.nonsingular_iff' : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3) (size : ℕ)
  (rk : α) (rv : β rk) (rl rr : Std.DTreeMap.Internal.Impl α β)
  (h : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size)
  (h_1 :
    (h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
      motive Std.DTreeMap.Internal.Impl.leaf h)
  (h_2 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rl rr : Std.DTreeMap.Internal.Impl α β) →
            (h : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size) →
              motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h),
  (match Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h with
    | Std.DTreeMap.Internal.Impl.leaf, h => h_1 h
    | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => h_2 size rk rv rl rr h) =
    h_2 size rk rv rl rr h
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.ULiftT.run_bind : ∀ {n : Type (max u v) → Type v'} [inst : Monad n] {α β : Type u} {x : Std.Iterators.ULiftT n α}
  {f : α → Std.Iterators.ULiftT n β},
  (x >>= f).run = do
    let a ← x.run
    (f a.down).run
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_add_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y z : E), inner 𝕜 x (y + z) = inner 𝕜 x y + inner 𝕜 x z
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_of_isEmpty : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → m[a]? = none
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.isPrincipal_mul_omega : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) (Ordinal.omega o)
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_eq_zpow_neg_valuation : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : PadicSeq p}, ¬f ≈ 0 → f.norm = ↑p ^ (-f.valuation)
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_le_inter_add_sdiff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] (μ : F)
  (s t : Set α), μ s ≤ μ (s ∩ t) + μ (s \ t)
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.Integrable.add : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α →ₘ[μ] β}, f.Integrable → g.Integrable → (f + g).Integrable
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {fallback : β k} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getD k fallback = (f (t.get? k)).getD fallback
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfEquivalence_inv_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasLimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasLimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfEquivalence e w).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G (e.functor.obj j))
      (CategoryTheory.CategoryStruct.comp (w.hom.app j) h)
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.leftUnitor_inv_tensor_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).inv
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.forIn'_eq_foldlM.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (b : ForInStep β) → ((b : β) → motive (ForInStep.yield b)) → ((b : β) → motive (ForInStep.done b)) → motive b