mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.DocString
/-- Renders the name of a documentation `extension` (role, code block, directive, or command) for
user-facing messages. Builtins are designated by their last component because users invoke them by
that bare name (e.g. `` {given}`x` ``, rather than `` {Lean.Doc.given}`x` ``), regardless of which
namespaces are open. Non-builtin elements use `MessageData.ofConstName` so they appear in their
shortest unambiguous form.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.docElementMessage : Lean.Name → BaseIO Lean.MessageData
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.M.mk_surjective : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R))
  (m : ↑(ModuleCat.FilteredColimits.M F)), ∃ j x, ModuleCat.FilteredColimits.M.mk F ⟨j, x⟩ = m
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  (t t_1 : Std.ExtDTreeMap α β cmp), t = t_1 → ∀ (a : α) [inst_2 : Inhabited (β a)], t.get! a = t_1.get! a
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (xs : List ((a : α) × β a)) (h : xs.isEmpty = false),
  Std.Internal.List.minKey xs h = (Std.Internal.List.minKey? xs).get ⋯
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.mk : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] →
      (f g : ℝ → E) →
        (k : ℝ) →
          (ε : ℂ) →
            (f₀ g₀ : E) →
              MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
                MeasureTheory.LocallyIntegrableOn g (Set.Ioi 0) MeasureTheory.volume →
                  0 < k →
                    ε ≠ 0 →
                      (∀ x ∈ Set.Ioi 0, f (1 / x) = (ε * ↑(x ^ k)) • g x) →
                        (∀ (r : ℝ), (fun x => f x - f₀) =O[Filter.atTop] fun x => x ^ r) →
                          (∀ (r : ℝ), (fun x => g x - g₀) =O[Filter.atTop] fun x => x ^ r) → WeakFEPair E
-- Init.Data.Vector.Range
Vector.range'_succ : ∀ {s n step : ℕ}, Vector.range' s (n + 1) step = Vector.cast ⋯ (#v[s] ++ Vector.range' (s + step) n step)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.toUnfold.inj : ∀ {a a_1 : Lean.Name}, Lean.Meta.SimpEntry.toUnfold a = Lean.Meta.SimpEntry.toUnfold a_1 → a = a_1
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_neg : ∀ (n : ℤ), (-n).negOnePow = n.negOnePow
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.conjGL.eq_1 : ∀ (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (g : GL (Fin 2) ℝ),
  CongruenceSubgroup.conjGL Γ g =
    Subgroup.comap (Matrix.SpecialLinearGroup.mapGL ℝ)
      (ConjAct.toConjAct g⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ)
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- If the coefficient space is T2, then the power series is `tsum` of its monomials  -/
PowerSeries.as_tsum : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [T2Space R] (f : PowerSeries R),
  f = ∑' (d : ℕ), (PowerSeries.monomial d) ((PowerSeries.coeff d) f)
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
/-- A monoidal closed category is an enriched ordinary category over itself.  -/
CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.MonoidalClosed C] → CategoryTheory.EnrichedOrdinaryCategory C C
-- Mathlib.Algebra.Category.BialgCat.Basic
/-- The underlying type.  -/
BialgCat.carrier : {R : Type u} → [inst : CommRing R] → BialgCat R → Type v
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry!.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (size : ℕ) (k : α) (v : β)
  (l : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.maxEntry!
      (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) =
    (k, v)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Initial.left_inv' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Algebra F} (h : CategoryTheory.Limits.IsInitial A),
  { f := CategoryTheory.CategoryStruct.comp (CategoryTheory.Endofunctor.Algebra.Initial.strInv h) A.str, h := ⋯ } =
    CategoryTheory.CategoryStruct.id A
-- Mathlib.Order.PiLex
Pi.Colex.lt_iff_of_unique : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Unique ι] [inst_1 : (i : ι) → LT (β i)] [inst_2 : Preorder ι]
  {x y : Colex ((i : ι) → β i)}, x < y ↔ x default < y default
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for groups is fully faithful.
 -/
GrpCat.uliftFunctorFullyFaithful : GrpCat.uliftFunctor.FullyFaithful
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.findIdxNth.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → ℕ → Sort u_2) (a : α) (xs : List α) (n s : ℕ) (h_1 : (x s : ℕ) → motive [] x s)
  (h_2 : (a : α) → (xs : List α) → (s : ℕ) → motive (a :: xs) 0 s)
  (h_3 : (a : α) → (xs : List α) → (n s : ℕ) → motive (a :: xs) n.succ s),
  (match a :: xs, n.succ, s with
    | [], x, s => h_1 x s
    | a :: xs, 0, s => h_2 a xs s
    | a :: xs, n.succ, s => h_3 a xs n s) =
    h_3 a xs n s
-- Mathlib.GroupTheory.Finiteness
AddGroup.fg_def : ∀ {H : Type u_4} [inst : AddGroup H], AddGroup.FG H ↔ ⊤.FG
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSlice : (α : Type u_1) → [Ord α] → Type u_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- If `d : MultispanIndex J C` and `F : C ⥤ D`, this is the obvious isomorphism
`(d.map F).multispan ≅ d.multispan ⋙ F`.  -/
CategoryTheory.Limits.MultispanIndex.multispanMapIso : {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] →
        {J : CategoryTheory.Limits.MultispanShape} →
          (d : CategoryTheory.Limits.MultispanIndex J C) →
            (F : CategoryTheory.Functor C D) → (d.map F).multispan ≅ d.multispan.comp F
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffOn.eq_1 : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (n : WithTop ℕ∞) (f : M → M')
  (s : Set M), ContMDiffOn I I' n f s = ∀ x ∈ s, ContMDiffWithinAt I I' n f s x
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_le_one_iff : ∀ {r : NNReal}, ↑r ≤ 1 ↔ r ≤ 1
-- Mathlib.Topology.Category.TopCat.Sphere
/-- The `n`-disk is the set of points in ℝⁿ whose norm is at most `1`,
endowed with the subspace topology.  -/
TopCat.disk : ℕ → TopCat
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult : Type
-- Lean.Server.References
/-- Yields all references in `module` at `pos`.  -/
Lean.Server.References.findAt : Lean.Server.References → Lean.Name → Lean.Lsp.Position → optParam Bool false → Array Lean.Lsp.RefIdent
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- The image of `(0, 2π]` under `circleMap c R` is the circle with center `c` and radius `|R|`.  -/
image_circleMap_Ioc : ∀ (c : ℂ) (R : ℝ), circleMap c R '' Set.Ioc 0 (2 * Real.pi) = Metric.sphere c |R|
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.keys_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keys = t₂.keys
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instTransVeqVle : {R : Type u_1} →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → Trans ValuativeRel.veq ValuativeRel.vle ValuativeRel.vle
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.quotAnnihilatorEquiv_apply : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V)
  (φ : Module.Dual K V), W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = (Submodule.dualRestrict W) φ
-- Mathlib.Dynamics.Minimal
dense_of_nonempty_vadd_invariant : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α]
  [AddAction.IsMinimal M α] {s : Set α}, s.Nonempty → (∀ (c : M), c +ᵥ s ⊆ s) → Dense s
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.appr_lt : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ), x.appr n < p ^ n
-- Mathlib.Algebra.Module.FinitePresentation
/-- Given an exact sequence `0 → M → N → P → 0`
with `N` finitely presented and `P` projective, then `M` is also finitely presented.  -/
Module.finitePresentation_of_projective_of_exact : ∀ {R : Type u_2} {M : Type u_4} {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] {P : Type u_1} [inst_5 : AddCommGroup P] [inst_6 : Module R P]
  [Module.FinitePresentation R N] [Module.Projective R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P),
  Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → Module.FinitePresentation R M
-- Mathlib.Logic.Equiv.Defs
Equiv.cast_refl : ∀ {α : Sort u_1} (h : optParam (α = α) ⋯), Equiv.cast h = Equiv.refl α
-- Lean.DocString.Types
Lean.Doc.Block.blockquote.inj : ∀ {i : Type u} {b : Type v} {items items_1 : Array (Lean.Doc.Block i b)},
  Lean.Doc.Block.blockquote items = Lean.Doc.Block.blockquote items_1 → items = items_1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.property.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.property = 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.eq_empty_of_insertMany_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ},
  Std.ExtDHashMap.Const.insertMany m l = ∅ → m = ∅
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.sin_arctan_eq_zero : ∀ {x : ℝ}, Real.sin (Real.arctan x) = 0 ↔ x = 0
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_bot_top : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : BoundedOrder α] [inst_3 : Fintype α],
  Finset.Icc ⊥ ⊤ = Finset.univ
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.evalRingHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring Y] (x : X) (x_1 : LocallyConstant X Y),
  (LocallyConstant.evalRingHom x) x_1 = x_1 x
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight₁_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K], Height.logHeight₁ 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.associator_inv_app_apply : ∀ (K L M : SSet) {Δ : SimplexCategoryᵒᵖ}
  (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj K (CategoryTheory.MonoidalCategoryStruct.tensorObj L M)).obj Δ),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.associator (K.obj Δ) (L.obj Δ) (M.obj Δ)).inv)
      x =
    ((x.1, x.2.1), x.2.2)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xy_coprime : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), (Pell.xn a1 n).Coprime (Pell.yn a1 n)
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonIte : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Lean.Util.FoldConsts
_private.Lean.Util.FoldConsts.0.Lean.Expr.FoldConstsImpl.fold.visit : {α : Type} → (Lean.Name → α → α) → Lean.Expr → α → Lean.Expr.FoldConstsImpl.FoldM α
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.submoduleMap_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M₂] [inst_5 : TopologicalSpace M₂]
  {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃SL[σ₁₂] M₂) (p : Submodule R M) (x : ↥(Submodule.map (↑↑e) p)),
  ↑((e.submoduleMap p).symm x) = e.symm ↑x
-- Mathlib.CategoryTheory.Abelian.Basic
/-- the image of `f`  -/
CategoryTheory.Abelian.AbelianStruct.image : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Abelian.AbelianStruct f → C
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_le_ofReal : ∀ {K : Type u_1} [inst : RCLike K] {x y : ℝ}, ↑x ≤ ↑y ↔ x ≤ y
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.hasZeroObject_pUnit : CategoryTheory.Limits.HasZeroObject (CategoryTheory.Discrete PUnit.{u_1 + 1})
-- Mathlib.Logic.Function.OfArity
/-- Constant `n`-ary function with value `b`.  -/
Function.OfArity.const : (α : Type u) → {β : Type u} → β → (n : ℕ) → Function.OfArity α β n
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.bot_coe : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V], ↑⊥ = ∅
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_comap_uniformSpace : ∀ {β : Type v} {u : UniformSpace β} {α : Type u_1} {f : α → β} {l : Filter α}, Cauchy l ↔ Cauchy (Filter.map f l)
-- Batteries.Data.AssocList
Batteries.AssocList.toList_eraseP : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : Batteries.AssocList α β),
  (Batteries.AssocList.eraseP p l).toList =
    List.eraseP
      (fun x =>
        match x with
        | (a, b) => p a b)
      l.toList
-- Mathlib.Probability.Moments.SubGaussian
/-- **Alias** of `ProbabilityTheory.HasSubgaussianMGF.sum_of_hasCondSubgaussianMGF`.

---

Let `Y` be a random process strongly adapted to a filtration `ℱ`, such that for all `i : ℕ`,
`Y i` is conditionally sub-Gaussian with parameter `cY i` with respect to `ℱ (i - 1)`.
In particular, `n ↦ ∑ i ∈ range n, Y i` is a martingale.
Then the sum `∑ i ∈ range n, Y i` is sub-Gaussian with parameter `∑ i ∈ range n, cY i`.  -/
ProbabilityTheory.HasSubgaussianMGF_sum_of_HasCondSubgaussianMGF : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : StandardBorelSpace Ω] {Y : ℕ → Ω → ℝ}
  {cY : ℕ → NNReal} {ℱ : MeasureTheory.Filtration ℕ mΩ} [inst_1 : MeasureTheory.IsZeroOrProbabilityMeasure μ],
  MeasureTheory.StronglyAdapted ℱ Y →
    ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) μ →
      ∀ (n : ℕ),
        (∀ i < n - 1, ProbabilityTheory.HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
          ProbabilityTheory.HasSubgaussianMGF (fun ω => ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ
-- Mathlib.Tactic.GCongr.Core
/-- `gcongr_discharger` is used by `gcongr` to discharge side goals.

This is an extensible tactic using [`macro_rules`](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=tactic-macro-extension).
By default it calls `positivity` (after importing the `positivity` tactic).
Example: ``macro_rules | `(tactic| gcongr_discharger) => `(tactic| positivity)``.
 -/
Mathlib.Tactic.GCongr.tacticGcongr_discharger : Lean.ParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Constructor for isomorphisms in `P.Comma L R Q W` from isomorphisms of the left and right
components and naturality in the forward direction.  -/
CategoryTheory.MorphismProperty.Comma.isoMk : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {B : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
        {T : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      [inst_3 : Q.IsMultiplicative] →
                        [inst_4 : W.IsMultiplicative] →
                          [Q.RespectsIso] →
                            [W.RespectsIso] →
                              {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} →
                                (l : X.left ≅ Y.left) →
                                  (r : X.right ≅ Y.right) →
                                    autoParam
                                        (CategoryTheory.CategoryStruct.comp (L.map l.hom) Y.hom =
                                          CategoryTheory.CategoryStruct.comp X.hom (R.map r.hom))
                                        CategoryTheory.MorphismProperty.Comma.isoMk._auto_1 →
                                      (X ≅ Y)
-- Mathlib.Topology.VectorBundle.Constructions
instAddCommMonoidPullback : {B : Type u_3} →
  (E : B → Type u_5) →
    {B' : Type u_6} → (f : B' → B) → [i : (x : B) → AddCommMonoid (E x)] → (x : B') → AddCommMonoid ((f *ᵖ E) x)
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.eval_section_injective_of_eventually_injective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [CategoryTheory.IsCofilteredOrEmpty J] {j : J},
  (∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) →
    ∀ (i : J) (f : i ⟶ j), Function.Injective fun s => ↑s j
-- Init.Data.Int.DivMod.Basic
Int.natCast_ediv : ∀ (m n : ℕ), ↑(m / n) = ↑m / ↑n
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.hasSum_sub : ∀ {𝕜 : 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} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → ∀ {y : E}, y ∈ Metric.eball x r → HasSum (fun n => (p n) fun x_1 => y - x) (f y)
-- Mathlib.Algebra.Lie.Engel
LieSubmodule.exists_smul_add_of_span_sup_eq_top : ∀ {R : Type u₁} {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L}
  {x : L}, R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤ → ∀ (y : L), ∃ t, ∃ z ∈ I, y = t • x + z
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
/-- A constant bounding the norm of `μ s` for any set `s`.  -/
MeasureTheory.VectorMeasure.bound : {X : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] → {mX : MeasurableSpace X} → MeasureTheory.VectorMeasure X E → NNReal
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The `R`-submodule of continuous maps `α → M`.  -/
continuousSubmodule : (α : Type u_1) →
  [TopologicalSpace α] →
    (R : Type u_2) →
      [inst : Semiring R] →
        (M : Type u_3) →
          [inst_1 : TopologicalSpace M] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : Module R M] → [ContinuousConstSMul R M] → [IsTopologicalAddGroup M] → Submodule R (α → M)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology],
  h.rightHomologyIso =
    CategoryTheory.ShortComplex.rightHomologyMapIso' (CategoryTheory.Iso.refl S) S.rightHomologyData h
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Canon.State.mk.sizeOf_spec : ∀ (cache cacheInType : Std.HashMap Lean.Expr Lean.Expr),
  sizeOf { cache := cache, cacheInType := cacheInType } = 1 + sizeOf cache + sizeOf cacheInType
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instLocallyCompactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [LocallyCompactSpace α],
  LocallyCompactSpace (TopologicalSpace.NonemptyCompacts α)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from Lean expressions to their representations as `RingExpr`  -/
Lean.Meta.Grind.Arith.CommRing.Ring.denote : Lean.Meta.Grind.Arith.CommRing.Ring → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.RingExpr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolResult.syms : Lean.Lsp.DocumentSymbolResult → Array Lean.Lsp.DocumentSymbol
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.charPoly.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (E : LinearRecurrence R),
  E.charPoly = (Polynomial.monomial E.order) 1 - ∑ i, (Polynomial.monomial ↑i) (E.coeffs i)
-- Mathlib.Algebra.Ring.Parity
Odd.map : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : Semiring β] {a : α}
  [inst_2 : FunLike F α β] [RingHomClass F α β] (f : F), Odd a → Odd (f a)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- A *trail* is a walk with no repeating edges.  -/
SimpleGraph.Walk.IsTrail : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → Prop
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|`.  -/
Real.binEntropy_nonpos_of_nonpos : ∀ {p : ℝ}, p ≤ 0 → Real.binEntropy p ≤ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g)
  (e : Z ⟶ X) (he : CategoryTheory.CategoryStruct.comp e g = 0),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift g e he)
      (CategoryTheory.Limits.kernelIsoOfEq h).inv =
    CategoryTheory.Limits.kernel.lift f e ⋯
-- Mathlib.Topology.UnitInterval
Set.Icc.continuous_convexComb_prod : ∀ {a b : ℝ}, Continuous fun x => Set.Icc.convexComb x.1 x.2.1 x.2.2
-- Mathlib.Geometry.Polygon.Basic
/-- The `i`-th edge as an affine map `R →ᵃ[R] P`.  -/
Polygon.edgePath : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      {n : ℕ} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → [inst_3 : AddTorsor V P] → Polygon P n → Fin n → R →ᵃ[R] P
-- Mathlib.Data.FunLike.Fintype
/-- All `FunLike`s are finite if their domain and codomain are.

Non-dependent version of `DFunLike.fintype` that might be easier to infer.
This is not an instance because specific `FunLike` types might have a better-suited definition.
 -/
FunLike.fintype : (G : Type u_2) →
  {α : Type u_3} → {γ : Type u_4} → [FunLike G α γ] → [DecidableEq α] → [Fintype α] → [Fintype γ] → Fintype G
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.orthogonal_corootSpan_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], P.CorootForm.orthogonal (P.corootSpan R) = LinearMap.ker P.CorootForm
-- Mathlib.Order.Filter.Lift
Filter.lift'_pure : ∀ {α : Type u_1} {β : Type u_2} {h : Set α → Set β} {a : α}, Monotone h → (pure a).lift' h = Filter.principal (h {a})
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_iSup_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] {a : α} {f : ι → UpperSet α}, a ∈ ⨆ i, f i ↔ ∀ (i : ι), a ∈ f i
-- Mathlib.FieldTheory.SeparableDegree
/-- The minimal polynomial of an element of `E / F` of exponential characteristic `q` has
separable degree one if and only if the minimal polynomial is of the form
`X ^ (q ^ n) - C y` for some `n : ℕ` and `y : F`.  -/
minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Ring E] [IsDomain E] [inst_3 : Algebra F E] (q : ℕ)
  [hF : ExpChar F q] {x : E},
  (minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y