mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.fg_ker : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Finite R M] [h : Module.FinitePresentation R N]
  (l : M →ₗ[R] N), Function.Surjective ⇑l → l.ker.FG
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_top : ∀ {M : Type u_1} [inst : Monoid M], ⊤.units = ⊤
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.instZeroHomFunctor : {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] →
        [CategoryTheory.Preadditive D] → {F G : CategoryTheory.Functor C D} → Zero (F ⟶ G)
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropy_iUnion_of_finite : ∀ {X : Type u_1} {ι : Type u_2} [inst : UniformSpace X] [Finite ι] {T : X → X} {F : ι → Set X},
  Dynamics.coverEntropy T (⋃ i, F i) = ⨆ i, Dynamics.coverEntropy T (F i)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.mk.injEq : ∀ {X Y : AlgebraicGeometry.Scheme} (source : X.Opens) (dense_source : Dense ↑source) (target : Y.Opens)
  (dense_target : Dense ↑target) (iso : ↑source ≅ ↑target) (source_1 : X.Opens) (dense_source_1 : Dense ↑source_1)
  (target_1 : Y.Opens) (dense_target_1 : Dense ↑target_1) (iso_1 : ↑source_1 ≅ ↑target_1),
  ({ source := source, dense_source := dense_source, target := target, dense_target := dense_target, iso := iso } =
      { source := source_1, dense_source := dense_source_1, target := target_1, dense_target := dense_target_1,
        iso := iso_1 }) =
    (source = source_1 ∧ target = target_1 ∧ iso ≍ iso_1)
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- linear equivalences between `Module`s are the same as (isomorphic to) isomorphisms
in `SemimoduleCat`  -/
linearEquivIsoModuleIsoₛ : {R : Type u} →
  [inst : Semiring R] →
    {X Y : Type u} →
      [inst_1 : AddCommMonoid X] →
        [inst_2 : AddCommMonoid Y] →
          [inst_3 : Module R X] → [inst_4 : Module R Y] → (X ≃ₗ[R] Y) ≅ SemimoduleCat.of R X ≅ SemimoduleCat.of R Y
-- Mathlib.Topology.Order.OrderClosedExtr
/-- If `f` is antitone on `Ioc a b` and monotone on `Ico b c` then `f` has
a local minimum at `b`.  -/
isLocalMin_of_anti_mono : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {β : Type u_2}
  [inst_3 : Preorder β] {a b c : α},
  a < b → b < c → ∀ {f : α → β}, AntitoneOn f (Set.Ioc a b) → MonotoneOn f (Set.Ico b c) → IsLocalMin f b
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.expr.inj : ∀ {e e_1 : Lean.Expr},
  Lean.Elab.Tactic.ResolveSimpIdResult.expr e = Lean.Elab.Tactic.ResolveSimpIdResult.expr e_1 → e = e_1
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.ShortComplex.epi_of_mono_of_epi_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ShortComplex C} (φ : R₁ ⟶ R₂),
  R₁.Exact → CategoryTheory.Mono R₂.f → CategoryTheory.Epi φ.τ₂ → CategoryTheory.Mono φ.τ₃ → CategoryTheory.Epi φ.τ₁
-- Init.Data.Nat.Div.Lemmas
Nat.add_div_of_dvd_add_add_one : ∀ {c a b : ℕ}, c ∣ a + b + 1 → (a + b) / c = a / c + b / c
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.mk.injEq : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {X : C} {data : F.OneHypercoverDenseData J₀ J X} {X₀ : C₀}
  {f : F.obj X₀ ⟶ X} {Y₀ : C₀} {g : Y₀ ⟶ X₀} (i₀ : data.I₀) (q : F.obj Y₀ ⟶ F.obj (data.X i₀))
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp q (data.f i₀) = CategoryTheory.CategoryStruct.comp (F.map g) f)
      CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac._autoParam)
  (i₀_1 : data.I₀) (q_1 : F.obj Y₀ ⟶ F.obj (data.X i₀_1))
  (fac_1 :
    autoParam (CategoryTheory.CategoryStruct.comp q_1 (data.f i₀_1) = CategoryTheory.CategoryStruct.comp (F.map g) f)
      CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac._autoParam),
  ({ i₀ := i₀, q := q, fac := fac } = { i₀ := i₀_1, q := q_1, fac := fac_1 }) = (i₀ = i₀_1 ∧ q ≍ q_1)
-- Init.Data.List.Lemmas
List.flatten_flatten : ∀ {α : Type u_1} {L : List (List (List α))}, L.flatten.flatten = (List.map List.flatten L).flatten
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (X : CategoryTheory.Abelian.SpectralObject C ι)
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) [X.HasSpectralSequence data] (r r' : ℤ)
  (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq : κ),
  (∀ (pq' : κ), ¬(c r).Rel pq' pq) →
    ∀ (n : ℤ),
      n = data.deg pq - 1 →
        CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRcoSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRcoSlice._auto_1) →
    Std.Rco.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RcoSlice α)
-- Init.Grind.Ring.Basic
/-- A commutative semiring, i.e. a semiring with commutative multiplication.

Use `CommRing` if the type has negation.
 -/
Lean.Grind.CommSemiring : Type u → Type u
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.decidableLE.match_1.eq_1 : ∀ {α : Type u_1} (motive : WithTop α → WithTop α → Sort u_2) (x : WithTop α) (h_1 : (x : WithTop α) → motive none x)
  (h_2 : (a : α) → motive (some a) none) (h_3 : (a b : α) → motive (some a) (some b)),
  (match none, x with
    | none, x => h_1 x
    | some a, none => h_2 a
    | some a, some b => h_3 a b) =
    h_1 x
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasCoproducts : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  {inst_1 : Fact κ.IsRegular} {inst_2 : OrderBot κ.ord.ToType} [self : I.IsCardinalForSmallObjectArgument κ],
  CategoryTheory.Limits.HasCoproducts C
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_self_sub_of_tmod_eq : ∀ {a b c : ℤ}, a.tmod b = c → b ∣ a - c
-- Mathlib.Algebra.CharP.Lemmas
/-- The Frobenius map `x ↦ x ^ p`.  -/
frobenius : (R : Type u_3) → [inst : CommSemiring R] → (p : ℕ) → [ExpChar R p] → R →+* R
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.NamespaceEntry.mk : List Lean.Name → Lean.Syntax → Lean.Syntax → Array Lean.Lsp.DocumentSymbol → Lean.Server.FileWorker.NamespaceEntry
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_coe : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)],
  (↑s).piecewise f g = s.piecewise f g
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles are translation invariant.  -/
EuclideanGeometry.angle_const_vadd : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p₁ p₂ p₃ : P),
  EuclideanGeometry.angle (v +ᵥ p₁) (v +ᵥ p₂) (v +ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃
-- Init.Data.Rat.Lemmas
Rat.pow_zero : ∀ (q : ℚ), q ^ 0 = 1
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.UniqueSums.toIsLeftCancelAdd : ∀ {G : Type u} [inst : Add G] [UniqueSums G], IsLeftCancelAdd G
-- Mathlib.Order.Category.Semilat
SemilatSupCatEquivSemilatInfCat_functor : SemilatSupCatEquivSemilatInfCat.functor = SemilatSupCat.dual
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_eq_bot : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M),
  Function.Injective ⇑f → f.ker = ⊥
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.IterM.step_intermediateZip.match_3.splitter : {α₁ β₁ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α₁ m β₁] →
      (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3) →
        (memo : Option { out // ∃ it, it.IsPlausibleOutput out }) →
          (Unit → motive none) → ((out₁ : { out // ∃ it, it.IsPlausibleOutput out }) → motive (some out₁)) → motive memo
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp g h)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConstC.go : ℤ → ℕ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Order.WithBot
Equiv.withTopCongr_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : WithTop α), e.withTopCongr a = WithTop.map (⇑e) a
-- Mathlib.Data.Matrix.Mul
RingHom.map_dotProduct : ∀ {n : Type u_3} {R : Type u_7} {S : Type u_8} [inst : Fintype n] [inst_1 : NonAssocSemiring R]
  [inst_2 : NonAssocSemiring S] (f : R →+* S) (v w : n → R), f (v ⬝ᵥ w) = ⇑f ∘ v ⬝ᵥ ⇑f ∘ w
-- Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
GenContFract.of_convergence_epsilon : ∀ {K : Type u_1} (v : K) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorRing K]
  [Archimedean K], ∀ ε > 0, ∃ N, ∀ n ≥ N, |v - (GenContFract.of v).convs n| < ε
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.instCircularOrder : CircularOrder Real.Angle
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_modify_eq_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α} {f : β → β} {fallback : α}, (t.modify k f).minKeyD fallback = t.minKeyD fallback
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₂.eq_1 : ∀ (a a_1 : String.Pos.Raw), String.Pos.Raw.extract.go₂ [] a a_1 = []
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The underlying morphism  -/
CategoryTheory.AddMon.Hom.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {M N : CategoryTheory.AddMon C} → M.Hom N → (M.X ⟶ N.X)
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
CategoryTheory.preadditiveYonedaObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (Y : C) {X Y_1 : Cᵒᵖ}
  (f : X ⟶ Y_1),
  (CategoryTheory.preadditiveYonedaObj Y).map f =
    ModuleCat.ofHom { toFun := fun g => CategoryTheory.CategoryStruct.comp f.unop g, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Algebra.Hom.Rat
RingHom.equivRatAlgHom_symm_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (self : R →ₐ[ℚ] S), (RingHom.equivRatAlgHom R S).symm self = self.toRingHom
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Functor.pi'_eval : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (f : (i : I) → CategoryTheory.Functor A (C i)) (i : I),
  (CategoryTheory.Functor.pi' f).comp (CategoryTheory.Pi.eval C i) = f i
-- Mathlib.Order.Hom.Bounded
/-- The type of `⊥`-preserving functions from `α` to `β`.  -/
BotHom : (α : Type u_6) → (β : Type u_7) → [Bot α] → [Bot β] → Type (max u_6 u_7)
-- Mathlib.Topology.Constructions
DiscreteTopology.isDiscrete : ∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X} [DiscreteTopology ↑s], IsDiscrete s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.isPiSystem_Ioi_rat : IsPiSystem (⋃ a, {Set.Ioi ↑a})
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- A category has an initial object if it has a colimit over the empty diagram.
Use `hasInitial_of_unique` to construct instances.
 -/
CategoryTheory.Limits.HasInitial : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Std.Http.Data.Body.Empty
/-- An empty body handle.
 -/
Std.Http.Body.Empty : Type
-- Mathlib.SetTheory.Cardinal.Finite
Set.card_prod_singleton : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (b : β), Nat.card ↑(s ×ˢ {b}) = Nat.card ↑s
-- Aesop.Stats.Extension
Aesop.recordStatsForCurrentFileIfEnabled : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [Lean.MonadOptions m] → [Lean.MonadLog m] → Lean.Syntax → Aesop.Stats → m Unit
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.instInnerFibrationFromOfQuasicategory : ∀ {X : SSet} [X.Quasicategory], SSet.InnerFibration (CategoryTheory.Limits.terminal.from X)
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The leading coefficient of a product of polynomials is equal to
the product of the leading coefficients.

See `Polynomial.leadingCoeff_multiset_prod'` (with a `'`) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.
 -/
Polynomial.leadingCoeff_multiset_prod : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)),
  t.prod.leadingCoeff = (Multiset.map (fun f => f.leadingCoeff) t).prod
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.cardQuot_pow_inertiaDeg : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [Module.Finite R S] [p.IsMaximal] [q.IsMaximal] [q.LiesOver p],
  Submodule.cardQuot p ^ q.inertiaDeg R = Submodule.cardQuot q
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mul_iff_left : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : CommGroup β] [IsTopologicalGroup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    (MeasureTheory.AEStronglyMeasurable (g * f) μ ↔ MeasureTheory.AEStronglyMeasurable g μ)
-- Mathlib.Tactic.Coe
/-- Elaborator for the `(↑)`, `(⇑)`, and `(↥)` notations.  -/
Lean.Elab.Term.CoeImpl.elabPartiallyAppliedCoe : String → Lean.Expr → (Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr) → Lean.Elab.TermElabM Lean.Expr
-- Lean.Parser.Syntax
Lean.Parser.Syntax.atom.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.anyM_filterMap : ∀ {α β β' : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α Id m] [LawfulMonad m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β}
  {f : β → Option β'} {p : β' → m Bool},
  Std.Iter.anyM p (Std.Iter.filterMap f it) =
    Std.Iter.anyM
      (fun x =>
        match f x with
        | some fx => p fx
        | none => pure false)
      it
-- Mathlib.Data.Finset.Insert
Finset.subset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), s ⊆ insert a s
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A commuting square of isomorphisms induces an isomorphism of kernels.  -/
CategoryTheory.Limits.kernel.mapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            {X' Y' : C} →
              (f' : X' ⟶ Y') →
                [inst_3 : CategoryTheory.Limits.HasKernel f'] →
                  (p : X ≅ X') →
                    (q : Y ≅ Y') →
                      CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f' →
                        (CategoryTheory.Limits.kernel f ≅ CategoryTheory.Limits.kernel f')
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.mul_integral_comp_mul_left : ∀ {a b : ℝ} {f : ℝ → ℝ} (c : ℝ), c * ∫ (x : ℝ) in a..b, f (c * x) = ∫ (x : ℝ) in c * a..c * b, f x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_neg : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  W.Nonsingular P → WeierstrassCurve.Jacobian.Point.toAffine W (W.neg P) = -WeierstrassCurve.Jacobian.Point.toAffine W P
-- Mathlib.Algebra.FreeMonoid.Count
FreeAddMonoid.countP_apply : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : FreeAddMonoid α),
  (FreeAddMonoid.countP p) l = List.countP (fun b => decide (p b)) (FreeAddMonoid.toList l)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_zero : Ordinal.deriv 0 = id
-- Lean.Server.Completion.CompletionCollectors
/-- Return the auto-completion label if `id` can be auto completed using `declName` assuming namespace `ns` is open.
This function only succeeds with atomic labels. BTW, it seems most clients only use the last part.

Remark: `danglingDot == true` when the completion point is an identifier followed by `.`.
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.matchDecl? : Lean.Name → Lean.Name → Bool → Lean.Name → Lean.MetaM (Option Lean.Name)
-- Lean.Level
Lean.Level.addOffset : Lean.Level → ℕ → Lean.Level
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_erase_le : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (Polynomial.erase n p).degree ≤ p.degree
-- Batteries.Data.Fin.Coding
/-- Decode `PUnit` from `Fin 1`.  -/
Fin.decodePUnit : Fin 1 → PUnit.{u_1}
-- Mathlib.Data.Finset.Max
Finset.min_mem_insert_top_image_coe : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α), s.min ∈ insert ⊤ (Finset.image WithTop.some s)
-- Mathlib.FieldTheory.Finite.Basic
ZMod.pow_card_pow : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {n : ℕ} (x : ZMod p), x ^ p ^ n = x
-- Mathlib.Data.Multiset.Fintype
Multiset.toEmbedding_coeEquiv_trans : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α),
  m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype fun x => x ∈ m.toEnumFinset) = m.coeEmbedding
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.lt_floor_add_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (a : R), a < ↑⌊a⌋₊ + 1
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `TwoUniqueSums` is preserved under additive equivalences.  -/
AddEquiv.twoUniqueSums_iff : ∀ {G : Type u} {H : Type v} [inst : Add G] [inst_1 : Add H] (f : G ≃+ H), TwoUniqueSums G ↔ TwoUniqueSums H
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.addEquivProdDirectSum_apply : ∀ {ι : Type v} {α : Option ι → Type w} [inst : (i : Option ι) → AddCommMonoid (α i)]
  (f : Π₀ (i : Option ι), (fun i => α i) i), DirectSum.addEquivProdDirectSum f = (f none, DFinsupp.comapDomain some ⋯ f)
-- Mathlib.Algebra.Star.Unitary
/-- In a ring without zero divisors and with trivial star, the only unitary elements are `1`
and `-1`.  -/
Unitary.mem_iff_eq_one_or_eq_neg_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] [TrivialStar R] [NoZeroDivisors R] {a : R},
  a ∈ unitary R ↔ a = 1 ∨ a = -1
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Extract a lean expression from an `Obj` term.  -/
Mathlib.Tactic.BicategoryLike.Obj.e : Mathlib.Tactic.BicategoryLike.Obj → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_iso_inv_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).iso.inv.app X_1 =
    S.iso.inv.app (U.obj X_1)
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.category : {R : Type u} → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (CoalgCat R)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.le : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] (f : MeasureTheory.Filtration ι m) (i : ι),
  ↑f i ≤ m
-- Mathlib.Algebra.Group.Defs
isMulTorsionFree_iff : ∀ (M : Type u_2) [inst : Monoid M], IsMulTorsionFree M ↔ ∀ ⦃n : ℕ⦄, n ≠ 0 → Function.Injective fun a => a ^ n
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.countable_of_isDiscrete : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s → IsDiscrete s → s.Countable
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.toGL.eq_1 : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R],
  Matrix.SpecialLinearGroup.toGL =
    { toFun := fun A => { val := ↑A, inv := ↑A⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.apply_order_ne_zero : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F}, p ≠ 0 → p p.order ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.map_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type w} [inst_2 : LinearOrder J] [inst_3 : OrderBot J] {X Y : C} {f : X ⟶ Y} [inst_4 : SuccOrder J]
  [inst_5 : WellFoundedLT J] (c : CategoryTheory.TransfiniteCompositionOfShape J f) (F : CategoryTheory.Functor C D)
  [inst_6 : CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J F]
  [inst_7 : CategoryTheory.Limits.PreservesColimitsOfShape J F], (c.map F).F = c.F.comp F
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.prop_id : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} (self : D.IsTerminal e),
  D.W (CategoryTheory.CategoryStruct.id e)
-- Mathlib.Logic.Function.Basic
/-- We can use choice to construct explicitly a partial inverse for
a given injective function `f`.  -/
Function.partialInv : {α : Type u_4} → {β : Sort u_5} → (α → β) → β → Option α
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.vecMul_surjective_iff_isUnit : ∀ {m : Type u} [inst : DecidableEq m] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Fintype m] {A : Matrix m m R},
  (Function.Surjective fun v => Matrix.vecMul v A) ↔ IsUnit A
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImport : Type
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.Channel.inner : {α : Type} → Std.Channel α → Std.CloseableChannel α
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtensionAlongEquivalence : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D] {L : C ≌ D}
  {F₀ : CategoryTheory.Functor C H} {F₁ : CategoryTheory.Functor D H} (α : L.functor.comp F₁ ≅ F₀),
  F₁.IsRightKanExtension α.hom