mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Function
ConvexOn.add_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : Module 𝕜 β] {s : Set E} {f : E → β}
  [IsOrderedAddMonoid β], ConvexOn 𝕜 s f → ∀ (b : β), ConvexOn 𝕜 s (f + fun x => b)
-- Mathlib.Tactic.CategoryTheory.Coherence.Basic
/-- List.splitEvenOdd [0, 1, 2, 3, 4] = ([0, 2, 4], [1, 3])  -/
Mathlib.Tactic.BicategoryLike.List.splitEvenOdd : {α : Type u} → List α → List α × List α
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.PrefixTable.step.match_1.eq_1 : ∀ {α : Type u_1} (t : Array.PrefixTable α) (motive : (k : ℕ) → k < t.size + 1 → Sort u_2) (hk : 0 < t.size + 1)
  (h_1 : (hk : 0 < t.size + 1) → motive 0 hk) (h_2 : (k : ℕ) → (hk : k + 1 < t.size + 1) → motive k.succ hk),
  (match 0, hk with
    | 0, hk => h_1 hk
    | k.succ, hk => h_2 k hk) =
    h_1 hk
-- Mathlib.LinearAlgebra.DFinsupp
/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere.

See note [partially-applied ext lemmas].
After applying this lemma, if `M = R` then it suffices to verify
`φ (single a 1) = ψ (single a 1)`.  -/
DFinsupp.lhom_ext' : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄,
  (∀ (i : ι), φ ∘ₗ DFinsupp.lsingle i = ψ ∘ₗ DFinsupp.lsingle i) → φ = ψ
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_lt : ∀ {a b : UInt32}, a.toUInt64 < b.toUInt64 ↔ a < b
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of Haar measures**:
Two Haar measures which are probability measures coincide.  -/
MeasureTheory.Measure.isHaarMeasure_eq_of_isProbabilityMeasure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure μ'] [μ.IsHaarMeasure] [μ'.IsHaarMeasure], μ' = μ
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.«term__ⁿ⁺¹» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.Module.LocallyConvex
LocallyConvexSpace.convex_basis : ∀ {𝕜 : Type u_1} {E : Type u_2} {inst : Semiring 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : AddCommMonoid E}
  {inst_3 : Module 𝕜 E} {inst_4 : TopologicalSpace E} [self : LocallyConvexSpace 𝕜 E] (x : E),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ Convex 𝕜 s) id
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariation.sum_le_preVariationFun_iUnion : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : ℕ → Set X},
  (∀ (i : ℕ), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      ∑' (i : ℕ), MeasureTheory.preVariationFun f (s i) ≤ MeasureTheory.preVariationFun f (⋃ i, s i)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp_zero : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (h : MeasureTheory.MemLp 0 p μ), MeasureTheory.MemLp.toLp 0 h = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.variable.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.variable = 1
-- Mathlib.RingTheory.Unramified.Locus
Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAtOfIsLiesOverAlgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (p : Ideal R)
  [inst_3 : p.IsPrime] (q : Ideal A) [inst_4 : q.IsPrime] [inst_5 : q.LiesOver p] [Algebra.IsUnramifiedAt R q]
  [inst_7 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)] [Localization.AtPrime.IsLiesOverAlgebra p q],
  Algebra.FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime q)
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- A bijection between the quotient of the action of an additive subgroup `H` on an
orbit, and a corresponding quotient expressed in terms of `Setoid.comap Subtype.val`.  -/
AddAction.equivAddSubgroupOrbitsSetoidComap : {G : Type u} →
  {X : Type v} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] →
        (H : AddSubgroup G) →
          (ω : Quotient (AddAction.orbitRel G X)) →
            AddAction.orbitRel.Quotient ↥H ↑(AddAction.orbitRel.Quotient.orbit ω) ≃
              Quotient (Setoid.comap Subtype.val (AddAction.orbitRel (↥H) X))
-- Mathlib.Algebra.Torsor.Basic
Prod.instTorsor : {G : Type u_1} →
  {G' : Type u_2} →
    {P : Type u_3} →
      {P' : Type u_4} →
        [inst : Group G] → [inst_1 : Group G'] → [Torsor G P] → [Torsor G' P'] → Torsor (G × G') (P × P')
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.moduleRight : {𝕜 : Type u_2} →
  {𝕝 : Type u_3} →
    {α : Type u_5} →
      [inst : Preorder α] →
        [inst_1 : Semiring 𝕜] → [inst_2 : AddCommMonoid 𝕝] → [Module 𝕜 𝕝] → Module 𝕜 (IncidenceAlgebra 𝕝 α)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.mk.injEq : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (toAffineMap : P →ᵃ[𝕜] P₂)
  (norm_map : ∀ (x : V), ‖toAffineMap.linear x‖ = ‖x‖) (toAffineMap_1 : P →ᵃ[𝕜] P₂)
  (norm_map_1 : ∀ (x : V), ‖toAffineMap_1.linear x‖ = ‖x‖),
  ({ toAffineMap := toAffineMap, norm_map := norm_map } = { toAffineMap := toAffineMap_1, norm_map := norm_map_1 }) =
    (toAffineMap = toAffineMap_1)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.named.injEq : ∀ (name : Lean.Name) (type default : Lean.Expr) (name_1 : Lean.Name) (type_1 default_1 : Lean.Expr),
  (Lean.Doc.ArgSpec.named✝ name type default = Lean.Doc.ArgSpec.named✝ name_1 type_1 default_1) =
    (name = name_1 ∧ type = type_1 ∧ default = default_1)
-- Mathlib.Data.Set.Monotone
AntitoneOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  AntitoneOn f s → s₂ ⊆ s → AntitoneOn f s₂
-- Lean.Data.NameMap.Basic
Lean.NameSSet.instEmptyCollection : EmptyCollection Lean.NameSSet
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.minEntry?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minEntry? = t₂.minEntry?
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.instMonadMor₂IsoMonoidalM : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso Mathlib.Tactic.Monoidal.MonoidalM
-- Std.Data.DHashMap.Raw
/-- Returns `true` if there is a mapping for the given key. There is also a `Prop`-valued version
of this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for comparisons, while for hash maps, both use `==`.
 -/
Std.DHashMap.Raw.contains : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → α → Bool
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_eq_mul_prod_sdiff_singleton_of_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∈ s → ∀ (f : ι → M), ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The morphism that is part of a morphism in `Under X`.  -/
CategoryTheory.Under.Hom.right : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → {X : T} → {f g : CategoryTheory.Under X} → (f ⟶ g) → (f.right ⟶ g.right)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roi.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roi α}, r.iter.toArray = r.toArray
-- Mathlib.Order.Restriction
/-- If a function `f` indexed by `α` is restricted to elements `≤ π`, and `a ≤ b`,
this is the restriction to elements `≤ a`.  -/
Preorder.restrictLe₂ : {α : Type u_1} →
  [inst : Preorder α] →
    {π : α → Type u_2} → {a b : α} → a ≤ b → ((a : ↑(Set.Iic b)) → π ↑a) → (a_1 : ↑(Set.Iic a)) → π ↑a_1
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_comp_inr : ∀ (R : Type u) {M : Type v} [inst : Zero R], TrivSqZeroExt.snd ∘ TrivSqZeroExt.inr = id
-- Mathlib.Analysis.Convolution
/-- Convolution is associative. This requires that
* all maps are a.e. strongly measurable w.r.t. one of the measures
* `f ⋆[L, ν] g` exists almost everywhere
* `‖g‖ ⋆[μ] ‖k‖` exists almost everywhere
* `‖f‖ ⋆[ν] (‖g‖ ⋆[μ] ‖k‖)` exists at `x₀`  -/
MeasureTheory.convolution_assoc : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF} {F' : Type uF'}
  {F'' : Type uF''} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup E'']
  [inst_3 : NormedAddCommGroup F] {f : G → E} {g : G → E'} [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedSpace 𝕜 E'] [inst_7 : NormedSpace 𝕜 E''] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedSpace 𝕜 F]
  [inst_10 : MeasurableSpace G] {μ ν : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [CompleteSpace F]
  [inst_12 : NormedAddCommGroup F'] [inst_13 : NormedSpace ℝ F'] [inst_14 : NormedSpace 𝕜 F'] [CompleteSpace F']
  [inst_16 : NormedAddCommGroup F''] [inst_17 : NormedSpace ℝ F''] [inst_18 : NormedSpace 𝕜 F''] [CompleteSpace F'']
  {k : G → E''} (L₂ : F →L[𝕜] E'' →L[𝕜] F') (L₃ : E →L[𝕜] F'' →L[𝕜] F') (L₄ : E' →L[𝕜] E'' →L[𝕜] F'')
  [inst_20 : AddGroup G] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [μ.IsAddRightInvariant] [MeasurableAdd₂ G]
  [ν.IsAddRightInvariant] [MeasurableNeg G],
  (∀ (x : E) (y : E') (z : E''), (L₂ (⋯ y)) z = (L₃ x) ((L₄ y) z)) →
    ∀ {x₀ : G},
      MeasureTheory.AEStronglyMeasurable f ν →
        MeasureTheory.AEStronglyMeasurable g μ →
          MeasureTheory.AEStronglyMeasurable k μ →
            (∀ᵐ (y : G) ∂μ, MeasureTheory.ConvolutionExistsAt f g y L ν) → (∀ᵐ (x : G) ∂ν, ⋯) → ⋯ → ⋯
-- Mathlib.Analysis.Convex.Slope
/-- If `f : 𝕜 → 𝕜` is convex, then for any three points `x < y < z` the slope of the secant line of
`f` on `[x, y]` is less than the slope of the secant line of `f` on `[y, z]`.  -/
ConvexOn.slope_mono_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multicospanIndexEnd_fst : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : (CategoryTheory.Limits.multicospanShapeEnd J).R),
  (CategoryTheory.Limits.multicospanIndexEnd F).fst f =
    (F.obj (Opposite.op (CategoryTheory.Arrow.left f))).map (CategoryTheory.Arrow.hom f)
-- Init.Data.String.Lemmas.Slice
String.Slice.instEquivBEq : EquivBEq String.Slice
-- Mathlib.Algebra.Star.StarAlgHom
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains.  -/
StarAlgHom.prodEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Star A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Star B] →
                      [inst_7 : Semiring C] →
                        [inst_8 : Algebra R C] → [inst_9 : Star C] → (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C) ≃ (A →⋆ₐ[R] B × C)
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- Given a quiver `V'` with reversible arrows, a prefunctor to `V'` can be lifted to one from
`Symmetrify V` to `V'`  -/
Quiver.Symmetrify.lift : {V : Type u_2} →
  [inst : Quiver V] →
    {V' : Type u_4} → [inst_1 : Quiver V'] → [Quiver.HasReverse V'] → V ⥤q V' → Quiver.Symmetrify V ⥤q V'
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.hasSum_integral_iUnion : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [Countable ι] {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      MeasureTheory.IntegrableOn f (⋃ i, s i) μ →
        HasSum (fun n => ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ n, s n, f x ∂μ)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.Edge.tensor_surjective : ∀ {X Y : SSet.Truncated 2}
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e : SSet.Truncated.Edge (x, y) (x', y')), ∃ e₁ e₂, e₁.tensor e₂ = e
-- Mathlib.Data.Fin.Basic
Fin.instCanLiftNatValLt : ∀ {n : ℕ}, CanLift ℕ (Fin n) Fin.val fun x => x < n
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.embDomain_injective : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'}, Function.Injective (HahnSeries.embDomain f)
-- Lean.Meta.Tactic.Ext
/-- The state of the `ext` extension environment  -/
Lean.Meta.Ext.ExtTheorems : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Complex.sinh` is complex analytic.  -/
Complex.analyticOnNhd_sinh : ∀ {s : Set ℂ}, AnalyticOnNhd ℂ Complex.sinh s
-- Aesop.RuleTac.Basic
Aesop.RuleTacInput.mk.injEq : ∀ (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId)
  (indexMatchLocations : Array Aesop.IndexMatchLocation) (patternSubsts? : Option (Array Aesop.Substitution))
  (options : Aesop.Options') (goal_1 : Lean.MVarId) (mvars_1 : Aesop.UnorderedArraySet Lean.MVarId)
  (indexMatchLocations_1 : Array Aesop.IndexMatchLocation) (patternSubsts?_1 : Option (Array Aesop.Substitution))
  (options_1 : Aesop.Options'),
  ({ goal := goal, mvars := mvars, indexMatchLocations := indexMatchLocations, patternSubsts? := patternSubsts?,
        options := options } =
      { goal := goal_1, mvars := mvars_1, indexMatchLocations := indexMatchLocations_1,
        patternSubsts? := patternSubsts?_1, options := options_1 }) =
    (goal = goal_1 ∧
      mvars = mvars_1 ∧
        indexMatchLocations = indexMatchLocations_1 ∧ patternSubsts? = patternSubsts?_1 ∧ options = options_1)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_top : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A], ↑⊤ = Set.univ
-- Lean.Elab.Tactic.Try
/-- Adds `tac` to `suggestions`.  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.appendSuggestion : Array (Lean.TSyntax `tactic) → Lean.TSyntax `tactic → Array (Lean.TSyntax `tactic)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Diffeomorph.preimage_boundary : ∀ {𝕜 : 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'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ (Φ : Diffeomorph I I' M N n), ⇑Φ ⁻¹' ModelWithCorners.boundary N = ModelWithCorners.boundary M
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.liftPrincipalSeg_top' : Ordinal.liftPrincipalSeg.top = Ordinal.type fun x1 x2 => x1 < x2
-- Mathlib.Probability.Process.Filtration
/-- If `ι` is a densely ordered linear order with no maximal element, then no point is isolated
on the right, so that `𝓕₊ i = ⨅ j > i, 𝓕 j` holds for all `i`. This is in particular the
case when `ι := ℝ≥0`.  -/
MeasureTheory.Filtration.rightCont_eq : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] [DenselyOrdered ι] [NoMaxOrder ι]
  (𝓕 : MeasureTheory.Filtration ι m) (i : ι), ↑𝓕.rightCont i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.mk.eq_1 : ∀ {M : Type u_1}, DomAddAct.mk = AddOpposite.opEquiv
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tildeEquiv_counitIso_hom_app_hom : ∀ {R : CommRingCat} (X : (SheafOfModules.isQuasicoherent (AlgebraicGeometry.Spec R).ringCatSheaf).FullSubcategory),
  (AlgebraicGeometry.tildeEquiv.counitIso.hom.app X).hom = AlgebraicGeometry.Scheme.Modules.fromTildeΓ X.obj
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat : {α : Type u_1} → [Lean.Grind.Field α] → ℚ → α
-- Mathlib.Combinatorics.Derangements.Finite
numDerangements_succ : ∀ (n : ℕ), ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F],
  CategoryTheory.CategoryStruct.comp (L.pointwiseLeftKanExtensionUnit (F.comp G))
      (L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.pointwiseLeftKanExtensionUnit F) G)
      (L.associator (L.pointwiseLeftKanExtension F) G).hom
-- Init.Data.String.Slice
/-- If `pat` matches a prefix of `s`, returns the remainder. Returns `s` unmodified
otherwise.

Use `String.Slice.dropPrefix?` to return `none` when `pat` does not match a prefix.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".toSlice.dropPrefix "red " == "green blue".toSlice`

* `"red green blue".toSlice.dropPrefix "reed " == "red green blue".toSlice`

* `"red green blue".toSlice.dropPrefix 'r' == "ed green blue".toSlice`

* `"red green blue".toSlice.dropPrefix Char.isLower == "ed green blue".toSlice`
 -/
String.Slice.dropPrefix : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → String.Slice
-- Mathlib.Topology.MetricSpace.Polish
/-- A set in a topological space is clopenable if there exists a finer Polish topology for which
this set is open and closed. It turns out that this notion is equivalent to being Borel-measurable,
but this is nontrivial (see `isClopenable_iff_measurableSet`).  -/
PolishSpace.IsClopenable : {α : Type u_1} → [t : TopologicalSpace α] → Set α → Prop
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  {v : β k} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.get a ⋯
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `L/E/K` is a tower of fields, then the spectral norm of `x : E` equals its spectral norm
when regarding `x` as an element of `L`.  -/
spectralNorm.eq_of_tower : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {E : Type u_4}
  [inst_3 : Field E] [inst_4 : Algebra K E] [inst_5 : Algebra E L] [IsScalarTower K E L] (x : E),
  spectralNorm K E x = spectralNorm K L ((algebraMap E L) x)
-- Lean.Server.Completion.CompletionResolution
/-- Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`.
 -/
Lean.Lsp.CompletionItem.resolve : Lean.Lsp.CompletionItem → Lean.Lsp.CompletionIdentifier → Lean.MetaM Lean.Lsp.CompletionItem
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.liftOrderTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PartialOrder β] {l : α → β}
  {u : β → α} (gc : GaloisConnection u l), gc.liftOrderTop = { top := l ⊤, le_top := ⋯ }
-- Init.Data.SInt.Basic
/-- Multiplies two 16-bit signed integers, wrapping around on over- or underflow.  Usually accessed via
the `*` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.mul : Int16 → Int16 → Int16
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.isConj_swap : ∀ {α : Type u} [inst : DecidableEq α] {w x y z : α}, w ≠ x → y ≠ z → IsConj (Equiv.swap w x) (Equiv.swap y z)
-- Mathlib.Order.Filter.Basic
Filter.Eventually.ne_of_lt : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g : α → β},
  (∀ᶠ (x : α) in l, f x < g x) → ∀ᶠ (x : α) in l, f x ≠ g x
-- Mathlib.RingTheory.LocalRing.Pullback
/-- The second projection from the pullback of `f : R →+* T` and `g : S →+* T` to `S`.  -/
RingHom.pullbackSnd : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : Ring R] →
        [inst_1 : Ring S] → [inst_2 : Semiring T] → (f : R →+* T) → (g : S →+* T) → ↥(f.pullback g) →+* S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.keyAtIdx?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keyAtIdx? i = t₂.keyAtIdx? i
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- A Z-group is a group whose Sylow subgroups are all cyclic.  -/
IsZGroup : (G : Type u_1) → [Group G] → Prop
-- Mathlib.MeasureTheory.Measure.EverywherePos
MeasureTheory.Measure.IsEverywherePos.smul_measure_nnreal : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  μ.IsEverywherePos s → ∀ {c : NNReal}, c ≠ 0 → (c • μ).IsEverywherePos s
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedOneHom : {M : Type u_4} → {N : Type u_5} → [inst : One M] → [inst_1 : One N] → Inhabited (OneHom M N)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- Tilde as a functor  -/
AlgebraicGeometry.tilde.functor : (R : CommRingCat) → CategoryTheory.Functor (ModuleCat ↑R) (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsStrictMinor.ne : ∀ {α : Type u_1} {M N : Matroid α}, N <m M → N ≠ M
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.card_pos : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S}, φ.IsArithFrobAt Q → 0 < Nat.card (R ⧸ Ideal.under R Q)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_mul : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f g : CauSeq β abv),
  CauSeq.Completion.mk f * CauSeq.Completion.mk g = CauSeq.Completion.mk (f * g)
-- Init.Data.Nat.Lemmas
Nat.mul_div_right_comm : ∀ {a b : ℕ}, b ∣ a → ∀ (c : ℕ), a * c / b = a / b * c
-- Mathlib.Combinatorics.Hindman
/-- `FS a` is the set of finite sums in `a`, i.e. `m ∈ FS a` if `m` is the sum of a nonempty
subsequence of `a`. We give a direct inductive definition instead of talking about subsequences.  -/
Hindman.FS : {M : Type u_1} → [AddSemigroup M] → Stream' M → Set M