mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.lanPresheafNatIso_hom_app : ∀ {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)}
  (hF :
    (S : LightProfinite) →
      CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))
  (S : LightProfiniteᵒᵖ),
  (LightCondensed.lanPresheafNatIso hF).hom.app S =
    CategoryTheory.Limits.colimit.desc
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op (Opposite.unop S))).comp
        (FintypeCat.toLightProfinite.op.comp F))
      (LightProfinite.Extend.cocone F (Opposite.unop S))
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `differentiable_const_add_iff`. -/
Differentiable.const_add : ∀ {𝕜 : 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] {f : E → F}
  (c : F), Differentiable 𝕜 f → Differentiable 𝕜 fun y => c + f y
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instInhabitedOrdinal : Inhabited Std.Time.Week.OfYear.Ordinal
-- Mathlib.Topology.Sheaves.Points
Opens.instSubsingletonObjOpensFiber : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) (Φ : (Opens.grothendieckTopology X).Point),
  Subsingleton (Φ.fiber.obj U)
-- Init.Data.Queue
Std.Queue.mk.injEq : ∀ {α : Type u} (eList dList eList_1 dList_1 : List α),
  ({ eList := eList, dList := dList } = { eList := eList_1, dList := dList_1 }) = (eList = eList_1 ∧ dList = dList_1)
-- Mathlib.Order.Filter.Pointwise
Filter.Tendsto.mul_mul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MulOneClass α] [inst_1 : MulOneClass β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β},
  Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) g₁ g₂ → Filter.Tendsto (⇑m) (f₁ * g₁) (f₂ * g₂)
-- Lean.LocalContext
Lean.LocalContext.empty : Lean.LocalContext
-- Mathlib.Logic.Basic
congr_arg_heq : ∀ {α : Sort u_1} {β : α → Sort u_2} (f : (a : α) → β a) {a₁ a₂ : α}, a₁ = a₂ → f a₁ ≍ f a₂
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- MetavarContext before the flexible tactic  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.mctx : Mathlib.Linter.Flexible.StainData✝ → Lean.MetavarContext
-- Mathlib.Tactic.Linter.FindDeprecations
/-- The output is the `HashMap` whose keys are the names of the files containing
deprecated declarations, and whose values are the arrays of ranges
corresponding to the deprecated declarations in that file.
The input `oldDate` and `newDate` are strings of the form "YYYY-MM-DD".
The output contains all the declarations that were deprecated after `oldDate`
and before `newDate`.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.deprecatedHashMap : String →
  String → Lean.Elab.Command.CommandElabM (Std.HashMap (Lean.Name × String) (Array (Lean.Name × Lean.Syntax.Range)))
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Nonempty.csInf_mem : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}, s.Nonempty → s.Finite → sInf s ∈ s
-- Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
minimalPrimes.finite_of_isNoetherianRing : ∀ (R : Type u_1) [inst : CommSemiring R] [hR : IsNoetherianRing R], (minimalPrimes R).Finite
-- Init.Data.Vector.Count
Vector.count_push : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} {a b : α} {xs : Vector α n},
  Vector.count a (xs.push b) = Vector.count a xs + if (b == a) = true then 1 else 0
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instNontrivialOfFactLtNatOfNat : ∀ {q : ℕ} [Fact (1 < q)], Nontrivial (LucasLehmer.X q)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.analyticWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → AnalyticWithinAt 𝕜 f s x
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.isRflTheorem : Lean.Name → Lean.CoreM Bool
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.not.inj : ∀ {α : Type} {a a_1 : Std.Tactic.BVDecide.BoolExpr α}, a.not = a_1.not → a = a_1
-- Mathlib.Logic.Function.Conjugate
/-- If `f` semiconjugates `ga` to `gb` and `f'` is both a left and a right inverse of `f`,
then `f'` semiconjugates `gb` to `ga`.  -/
Function.Semiconj.inverse_left : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α} {gb : β → β} {f' : β → α},
  Function.Semiconj f ga gb → Function.LeftInverse f' f → Function.RightInverse f' f → Function.Semiconj f' gb ga
-- Mathlib.RingTheory.AdicCompletion.Basic
isAdicComplete_iff : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsAdicComplete I M ↔ IsHausdorff I M ∧ IsPrecomplete I M
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.go_succ : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x₁ x₂ : α} {a₁ a₂ : List α} {i : ℕ},
  Array.compareLex.go✝ cmp (x₁ :: a₁).toArray (x₂ :: a₂).toArray (i + 1) =
    Array.compareLex.go✝ cmp a₁.toArray a₂.toArray i
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.hasLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} J]
  (X : C) (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X))
  [CategoryTheory.Limits.HasLimit (F.comp (CategoryTheory.Over.isMono X).ι)], CategoryTheory.Limits.HasLimit F
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidOpenTextDocumentParams.textDocument : Lean.Lsp.DidOpenTextDocumentParams → Lean.Lsp.TextDocumentItem
-- Mathlib.Order.SupClosed
isSublattice_preimage_ofDual : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, IsSublattice (⇑OrderDual.ofDual ⁻¹' s) ↔ IsSublattice s
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (p : X = Y),
  CategoryTheory.eqToIso p = CategoryTheory.eqToIso p
-- Mathlib.Order.Defs.Unbundled
refl_def : ∀ {α : Sort u_1} {r : α → α → Prop}, Std.Refl r ↔ ∀ ⦃a : α⦄, r a a
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The restriction of an isomorphism of graphs to induced subgraphs.  -/
SimpleGraph.Iso.induce : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} →
      {G' : SimpleGraph W} →
        {s : Set V} →
          {t : Set W} → (φ : G ≃g G') → Set.BijOn (⇑φ) s t → SimpleGraph.induce s G ≃g SimpleGraph.induce t G'
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitOfConeRightOpOfCocone_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneRightOpOfCocone c))
  (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.isColimitOfConeRightOpOfCocone F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.subgroup_strictAntiOn : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  StrictAntiOn MulArchimedeanClass.subgroup (Set.Iio ⊤)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.State.activeScopes : {σ : Type} → Lean.ScopedEnvExtension.State σ → Lean.NameSet
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.measurable_bind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ]
  (f : MeasureTheory.SimpleFunc α β) (g : β → α → γ), (∀ (b : β), Measurable (g b)) → Measurable fun a => g (f a) a
-- Std.Async.Basic
/-- Maps the result of a `BaseAsync` computation with a function.
 -/
Std.Async.BaseAsync.map : {α β : Type} →
  (α → β) →
    Std.Async.BaseAsync α → optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.BaseAsync β
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.stalkMap_surjective`.

---

**Alias** of `AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective`. -/
AlgebraicGeometry.SurjectiveOnStalks.surj_on_stalks : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.SurjectiveOnStalks f] (x : ↥X),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Init.Grind.Lemmas
Lean.Grind.Bool.eq_true_of_not_eq_false' : ∀ {a : Bool}, ¬a = false → a = true
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_le_subst_nonneg : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_le_subst_nonneg_cert x p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ = 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
/-- Two vertices are `k`-edge-reachable if they remain reachable after removing strictly fewer than
`k` edges.  -/
SimpleGraph.IsEdgeReachable : {V : Type u_1} → SimpleGraph V → ℕ → V → V → Prop
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_smulBasis_left : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) {G : Type u_7}
  [inst_8 : Group G] [inst_9 : DistribMulAction G M₁] [inst_10 : SMulCommClass G R M₁] (g : G) (f : M₁ →ₗ[R] M₂),
  (LinearMap.toMatrix (g • v₁) v₂) f = (LinearMap.toMatrix v₁ v₂) (f ∘ₗ DistribSMul.toLinearMap R M₁ g)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PreDiscrTree.mk.injEq : ∀ {α : Type} (roots : Std.HashMap Lean.Meta.LazyDiscrTree.Key ℕ)
  (tries : Array (Array (Lean.Meta.LazyDiscrTree.LazyEntry α))) (roots_1 : Std.HashMap Lean.Meta.LazyDiscrTree.Key ℕ)
  (tries_1 : Array (Array (Lean.Meta.LazyDiscrTree.LazyEntry α))),
  ({ roots := roots, tries := tries } = { roots := roots_1, tries := tries_1 }) = (roots = roots_1 ∧ tries = tries_1)
-- Lean.Parser.Command
Lean.Parser.Command.check_failure.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.comp_zero : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] (f : β →+o γ), f.comp 0 = 0
-- Mathlib.Algebra.Ring.Subring.Basic
RingHom.mem_range_self : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) (x : R), f x ∈ f.range
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.start_isSpecial : ∀ (a b : ℕ+), (PNat.XgcdType.start a b).IsSpecial
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- First-column Laplace expansion of a bordered minor  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.det_bordered_expand : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ} (α : Fin (p + 1) → Fin n)
  (i j : Fin n),
  BirdDet.bminor✝ A i j α = BirdDet.pminor✝ A α * A i j - ∑ s, BirdDet.bminor✝ A i (α s) (s.removeNth α) * A (α s) j
-- Lean.Util.Diff
/-- Delete the item from the source  -/
Lean.Diff.Action.delete : Lean.Diff.Action
-- Mathlib.Analysis.Normed.Order.UpperLower
IsUpperSet.thickening : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {s : Set α},
  IsUpperSet s → ∀ (ε : ℝ), IsUpperSet (Metric.thickening ε s)
-- Mathlib.Data.Nat.Find
Nat.findGreatest.eq_1 : ∀ (P : ℕ → Prop) [inst : DecidablePred P], Nat.findGreatest P 0 = 0
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.coconePointwiseProduct_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type u_1} {I : α → Type u_2}
  [inst_1 : (i : α) → CategoryTheory.Category.{v_1, u_2} (I i)] [inst_2 : CategoryTheory.Limits.HasProductsOfShape α C]
  {F : (i : α) → CategoryTheory.Functor (I i) C} (c : (i : α) → CategoryTheory.Limits.Cocone (F i)),
  (CategoryTheory.Limits.coconePointwiseProduct c).pt = ∏ᶜ fun i => (c i).pt
-- Mathlib.LinearAlgebra.Span.Defs
Module.isPrincipal_submodule_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p : Submodule R M}, Module.IsPrincipal R ↥p ↔ p.IsPrincipal
-- Batteries.Data.List.Basic
List.zipWithLeft'_eq_zipWithLeft'TR : @List.zipWithLeft' = @List.zipWithLeft'TR
-- Mathlib.Data.Ordering.Basic
/-- Lift a decidable relation to an `Ordering`,
assuming that incomparable terms are `Ordering.eq`.
 -/
cmpUsing : {α : Type u} → (lt : α → α → Prop) → [DecidableRel lt] → α → α → Ordering
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoordReal_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (p : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℝ × ℝ)),
  ↑(NumberField.mixedEmbedding.polarCoordReal K) p = (p.1, Pi.map (fun i => ↑polarCoord) p.2)
-- Mathlib.Analysis.Convex.Hull
/-- The convex hull of a set `s` is the minimal convex set that includes `s`.  -/
convexHull : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : Semiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : AddCommMonoid E] → [Module 𝕜 E] → ClosureOperator (Set E)
-- Std.Tactic.BVDecide.Syntax
Lean.Elab.Tactic.BVDecide.SolverMode.default.sizeOf_spec : sizeOf Lean.Elab.Tactic.BVDecide.SolverMode.default = 1
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.normalizedDerivOfComplex_mul : ∀ (F G : UpperHalfPlane → ℂ),
  MDiff F →
    MDiff G →
      Derivative.normalizedDerivOfComplex (F * G) =
        Derivative.normalizedDerivOfComplex F * G + F * Derivative.normalizedDerivOfComplex G
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.commutant.eq_1 : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (S : VonNeumannAlgebra H),
  S.commutant = { toStarSubalgebra := StarSubalgebra.centralizer ℂ ↑S, centralizer_centralizer' := ⋯ }
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The second derivative in terms `lineDerivOp` as a bilinear map.

Mainly used to give an abstract definition of the Laplacian.  -/
LineDeriv.bilinearLineDerivTwo : (R : Type u_4) →
  {E : Type u_6} →
    {V₁ : Type u_8} →
      {V₂ : Type u_9} →
        {V₃ : Type u_10} →
          [inst : LineDeriv E V₁ V₂] →
            [inst_1 : LineDeriv E V₂ V₃] →
              [inst_2 : AddCommGroup V₁] →
                [inst_3 : AddCommGroup V₂] →
                  [inst_4 : AddCommGroup V₃] →
                    [inst_5 : CommRing R] →
                      [inst_6 : AddCommGroup E] →
                        [inst_7 : Module R E] →
                          [inst_8 : Module R V₂] →
                            [inst_9 : Module R V₃] →
                              [LineDerivAdd E V₂ V₃] →
                                [LineDerivAdd E V₁ V₂] →
                                  [LineDerivSMul R E V₂ V₃] →
                                    [LineDerivLeftSMul R E V₁ V₂] →
                                      [LineDerivLeftSMul R E V₂ V₃] → V₁ → E →ₗ[R] E →ₗ[R] V₃
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_tan_ofReal_re : ∀ (x : ℝ), ↑(Complex.tan ↑x).re = Complex.tan ↑x
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceE_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₂₃ : j ⟶ l)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceE._auto_3),
  (X.kernelSequenceE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂₃)
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- Decompose `WithLp 2 (U × V) ≃ᵐ U × V` into a series of known measure-preserving equivalences  -/
_private.Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace.0.volumePreservingSymmMeasurableEquivToLpProdAux : (U : Type u_4) →
  (V : Type u_5) →
    [inst : NormedAddCommGroup U] →
      [inst_1 : InnerProductSpace ℝ U] →
        [inst_2 : MeasurableSpace U] →
          [BorelSpace U] →
            [FiniteDimensional ℝ U] →
              [inst : NormedAddCommGroup V] →
                [inst_4 : InnerProductSpace ℝ V] →
                  [inst_5 : MeasurableSpace V] → [BorelSpace V] → [FiniteDimensional ℝ V] → WithLp 2 (U × V) ≃ᵐ U × V
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.coe_one : ∀ (α : Type u_1) [inst : Ring α] [inst_1 : UniformSpace α], ↑1 = 1
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.frequently_le_mul : ∀ {u : ℕ → EReal} {a : EReal}, LinearGrowth.linearGrowthInf u < a → ∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ a * ↑n
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Given a predefinition, return the variable names in the outermost lambdas.
Includes the “fixed prefix”.

The length of the returned array is also used to determine the arity
of the function, so it should match what `packDomain` does.
 -/
Lean.Elab.WF.GuessLex.originalVarNames : Lean.Elab.PreDefinition → Lean.MetaM (Array Lean.Name)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_const_mul_left_iff : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S] {g : α → F}
  {l : Filter α} {f : α → S} {c : S}, c ≠ 0 → ((fun x => c * f x) =o[l] g ↔ f =o[l] g)
-- Mathlib.Topology.Separation.Basic
ULift.instT1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], T1Space (ULift.{u_3, u_1} X)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.LaxMonoidal] [adj.IsMonoidal], CategoryTheory.NatTrans.IsMonoidal adj.counit
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_swap : ∀ {α : Type u} {n : ℕ} (a : α) (x : Fin n → α) (i j : Fin n),
  Matrix.vecCons a (x ∘ ⇑(Equiv.swap i j)) = Matrix.vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.closure_sdiff_singleton_eq_closure`. -/
Matroid.closure_diff_singleton_eq_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α}, e ∈ M.closure (X \ {e}) → M.closure (X \ {e}) = M.closure X
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.of_le_left_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B → ∀ {A' : Subalgebra R S}, A' ≤ A → ∀ [Module.Flat R ↥B], A'.LinearDisjoint B
-- Mathlib.Topology.Separation.Regular
disjoint_lift'_closure_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T25Space X] {x y : X},
  Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure) ↔ x ≠ y
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_mono : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R], Monotone Int.ceil
-- Mathlib.RingTheory.Ideal.GoingUp
/-- **Alias** of `Ideal.IsIntegral.isMaximal_of_isMaximal_comap`. -/
Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] (I : Ideal A) [I.IsPrime], (Ideal.comap (algebraMap R A) I).IsMaximal → I.IsMaximal
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- If `f : ℂ → E` is complex differentiable on a closed disc of positive radius, then it is
analytic on the corresponding open disc, and the coefficients of the power series are given by
Cauchy integral formulas. See also
`Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable` for a version of this lemma with
weaker assumptions.  -/
DifferentiableOn.hasFPowerSeriesOnBall : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : NNReal} {c : ℂ}
  {f : ℂ → E},
  DifferentiableOn ℂ f (Metric.closedBall c ↑R) → 0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R
-- Mathlib.GroupTheory.Perm.Fin
Fin.insertNth_comp_cycleRange_symm : ∀ {n : ℕ} {α : Type u_1} (p : Fin (n + 1)) (a : α) (x : Fin n → α),
  p.insertNth a x ∘ ⇑(Equiv.symm p.cycleRange) = Fin.cons a x
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformly.exists : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β], SummableLocallyUniformly f → ∃ g, HasSumLocallyUniformly f g
-- Mathlib.Tactic.FunProp.ToBatteries
_private.Mathlib.Tactic.FunProp.ToBatteries.0.Mathlib.Meta.FunProp.betaThroughLetAux.match_1.eq_5 : ∀ (motive : Lean.Expr → List Lean.Expr → Sort u_1) (f : Lean.Expr) (args : List Lean.Expr)
  (h_1 : (f : Lean.Expr) → motive f [])
  (h_2 :
    (binderName : Lean.Name) →
      (binderType b : Lean.Expr) →
        (binderInfo : Lean.BinderInfo) →
          (a : Lean.Expr) → (as : List Lean.Expr) → motive (Lean.Expr.lam binderName binderType b binderInfo) (a :: as))
  (h_3 :
    (n : Lean.Name) →
      (t v b : Lean.Expr) → (nondep : Bool) → (args : List Lean.Expr) → motive (Lean.Expr.letE n t v b nondep) args)
  (h_4 : (data : Lean.MData) → (b : Lean.Expr) → (args : List Lean.Expr) → motive (Lean.Expr.mdata data b) args)
  (h_5 : (f : Lean.Expr) → (args : List Lean.Expr) → motive f args),
  (args = [] → False) →
    (∀ (binderName : Lean.Name) (binderType b : Lean.Expr) (binderInfo : Lean.BinderInfo) (a : Lean.Expr)
        (as : List Lean.Expr), f = Lean.Expr.lam binderName binderType b binderInfo → args = a :: as → False) →
      (∀ (n : Lean.Name) (t v b : Lean.Expr) (nondep : Bool), f = Lean.Expr.letE n t v b nondep → False) →
        (∀ (data : Lean.MData) (b : Lean.Expr), f = Lean.Expr.mdata data b → False) →
          (match f, args with
            | f, [] => h_1 f
            | Lean.Expr.lam binderName binderType b binderInfo, a :: as => h_2 binderName binderType b binderInfo a as
            | Lean.Expr.letE n t v b nondep, args => h_3 n t v b nondep args
            | Lean.Expr.mdata data b, args => h_4 data b args
            | f, args => h_5 f args) =
            h_5 f args
-- Lean.Parser.Basic
Lean.Parser.anyOfFn : List Lean.Parser.Parser → Lean.Parser.ParserFn
-- Aesop.Stats.Basic
Aesop.ForwardStateStats.mk.inj : ∀ {ruleStateStats ruleStateStats_1 : Array Aesop.ForwardRuleStateStats},
  { ruleStateStats := ruleStateStats } = { ruleStateStats := ruleStateStats_1 } → ruleStateStats = ruleStateStats_1
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_of_natDegree_le_one : ∀ {R : Type u_1} [inst : Field R] {f g : Polynomial R}, f.Splits → g.natDegree ≤ 1 → (f.comp g).Splits
-- Mathlib.Logic.Relation
Relation.transitive_transGen : ∀ {α : Type u_1} {r : α → α → Prop}, IsTrans α (Relation.TransGen r)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_curry : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α × β → M),
  Function.HasFiniteSupport f → ∑ᶠ (ab : α × β), f ab = ∑ᶠ (a : α) (b : β), f (a, b)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_def' : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} (ω : E → E →L[𝕜] F)
  (γ : Path a b) (t : ℝ), curveIntegralFun ω γ t = (ω (γ.extend t)) (derivWithin (⇑γ.extend) unitInterval t)