mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.body.injEq : ∀ (name : Lean.Name) (next : Mathlib.Tactic.Conv.Path) (name_1 : Lean.Name) (next_1 : Mathlib.Tactic.Conv.Path),
  (Mathlib.Tactic.Conv.Path.body name next = Mathlib.Tactic.Conv.Path.body name_1 next_1) =
    (name = name_1 ∧ next = next_1)
-- Mathlib.Topology.Category.Stonean.Basic
/-- The underlying `CompHaus` of a `Stonean`.  -/
Stonean.compHaus : Stonean → CompHaus
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearIndependent.cardinal_lift_le_rank : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {ι : Type w} {v : ι → M},
  LinearIndependent R v → Cardinal.lift.{v, w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, v} (Module.rank R M)
-- Mathlib.Topology.Constructible
Homeomorph.mk.congr_simp : ∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (toEquiv toEquiv_1 : X ≃ Y)
  (e_toEquiv : toEquiv = toEquiv_1) (continuous_toFun : Continuous toEquiv.toFun)
  (continuous_invFun : Continuous toEquiv.invFun),
  { toEquiv := toEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    { toEquiv := toEquiv_1, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Topology.Closure
Set.Finite.closure_biUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type u_1} {s : Set ι},
  s.Finite → ∀ (f : ι → Set X), closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)
-- Lean.Message
Lean.addMessageContextFull : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadMCtx m] → [Lean.MonadLCtx m] → [Lean.MonadOptions m] → Lean.MessageData → m Lean.MessageData
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toAddSubmonoid_strictMono : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  StrictMono Submodule.toAddSubmonoid
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ}, m.WF → (Std.HashMap.Raw.map f m).size = m.size
-- Init.Data.String.TakeDrop
/-- Checks whether a string only consists of matches of the pattern `pat`, starting from the back
of the string.

Short-circuits at the first pattern mis-match.

This function is generic over all currently supported patterns.

For many types of patterns, this function can be expected to return the same result as
`String.all`. If mismatches are expected to occur close to the end of the string, this function
might be more efficient.

For some types of patterns, this function will return a different result than `String.all`.
Consider, for example, a pattern that matches the longest string at the given position that matches
the regular expression `"a|aa|ab"`. Then, given the input string `"aab"`, performing
`String.all` will greedily match the prefix `"aa"` and then get stuck on the remainder
`"b"`, causing it to return `false`. On the other hand, `String.revAll` will match
the suffix `"ab"` and then match the remainder `"a"`, so it will return `true`.

Examples:

* `"brown".revAll Char.isLower = true`

* `"brown and orange".revAll Char.isLower = false`

* `"aaaaaa".revAll 'a' = true`

* `"aaaaaa".revAll "aa" = true`

* `"aaaaaaa".revAll "aa" = false`
 -/
String.revAll : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry!_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {a : α} [inst_1 : Inhabited ((a : α) × β a)],
  Std.Internal.List.getEntry! a [] = default
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCompletionItemKind.hash : Lean.Lsp.CompletionItemKind → UInt64
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.nonempty_isColimit_iff_eq_coinduced : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cocone F)
  (hc : CategoryTheory.Limits.IsColimit ((CategoryTheory.forget TopCat).mapCocone c)),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔
    c.pt.str = ⨆ j, TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Instances.Real.Lemmas
/-- A monotone, bounded above sequence `f : ℕ → ℝ` on `Ici k` has the finite
limit `sSup (f '' Ici k)`.  -/
Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici : ∀ {f : ℕ → ℝ} {k : ℕ},
  MonotoneOn f (Set.Ici k) → BddAbove (f '' Set.Ici k) → Filter.Tendsto f Filter.atTop (nhds (sSup (f '' Set.Ici k)))
-- Mathlib.RingTheory.FinitePresentation
RingHom.FinitePresentation.of_comp_finiteType : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  (f : A →+* B) {g : B →+* C}, (g.comp f).FinitePresentation → f.FiniteType → g.FinitePresentation
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
a cocone on `F` with cone point `W`.  -/
CategoryTheory.Limits.IsColimit.homEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit t → {W : C} → (t.pt ⟶ W) ≃ (F ⟶ (CategoryTheory.Functor.const J).obj W)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_injective : Function.Injective ENNReal.log
-- Mathlib.CategoryTheory.PEmpty
/-- Any two functors out of the empty category are *equal*. You probably want to use
`emptyExt` instead of this.
 -/
CategoryTheory.Functor.empty_ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F G : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C), F = G
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Iic_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) {c : α},
  c < 0 → (fun x => x * c) ⁻¹' Set.Iic a = Set.Ici (a / c)
-- Mathlib.Order.RelSeries
RelSeries.length_pos_of_nontrivial : ∀ {α : Type u_1} {r : SetRel α α} {s : RelSeries r}, {x | x ∈ s}.Nontrivial → 0 < s.length
-- Mathlib.GroupTheory.Sylow
Sylow.exists_comap_eq_of_ker_isPGroup : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (P : Sylow p H) {f : H →* G},
  IsPGroup p ↥f.ker → ∃ Q, Subgroup.comap f ↑Q = ↑P
-- Lean.Parser.Do
Lean.Parser.Term.nestedAction.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_neg_same' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable (fun x => Real.exp (f x)) μ → (μ.tilted f).tilted (-f) = (μ Set.univ)⁻¹ • μ
-- Mathlib.Topology.Compactness.Compact
Pi.compactSpace : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), CompactSpace (X i)],
  CompactSpace ((i : ι) → X i)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
/-- Naturality of the strong naturality constraint.  -/
CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (self : F.StrongTrans G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g)
  {Z : F.obj a ⟶ G.obj b} (h : CategoryTheory.CategoryStruct.comp (self.app a) (G.map g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b))
      (CategoryTheory.CategoryStruct.comp (self.naturality g).hom h) =
    CategoryTheory.CategoryStruct.comp (self.naturality f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η)) h)
-- Init.Omega.Constraint
Lean.Omega.Constraint.trivial_say : ∀ {t : ℤ}, Lean.Omega.Constraint.trivial.sat t = true
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [inst_3 : NeZero i] (hi : Even i)
  (x : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker),
  (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg i hi)) x = 0 ↔
    ↑x ∈ (Rep.Hom.hom A.norm).range
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.comap_incl_eq_bot : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N₂ : LieSubmodule R L M},
  LieSubmodule.comap N.incl N₂ = ⊥ ↔ N ⊓ N₂ = ⊥
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordCompl_div_of_dvd : ∀ {x p : ℕ}, Nat.Prime p → p ∣ x → x / p / p ^ (x / p).factorization p = x / p ^ x.factorization p
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
EReal.measurable_of_real_prod : ∀ {β : Type u_6} {γ : Type u_7} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {f : EReal × β → γ},
  (Measurable fun p => f (↑p.1, p.2)) → (Measurable fun x => f (⊥, x)) → (Measurable fun x => f (⊤, x)) → Measurable f
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R),
  x.map (CategoryTheory.CategoryStruct.id P) = x
-- Lean.Elab.DefView
Lean.Elab.instToSnapshotTreeHeaderProcessedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.HeaderProcessedSnapshot
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzWith_iff_norm_neg_add_le`. -/
LipschitzWith.norm_neg_add_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F} {C : NNReal},
  LipschitzWith C f → ∀ (x y : E), ‖-f x + f y‖ ≤ ↑C * ‖-x + y‖
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_eq_top : ∀ {M : Type u_2} [inst : Mul M] {S : Subsemigroup M}, S.op = ⊤ ↔ S = ⊤
-- Mathlib.Order.Atoms
bot_covBy_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, ⊥ ⋖ a ↔ IsAtom a
-- Mathlib.Algebra.Group.ForwardDiff
fwdDiff_smul : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (h : M) {R : Type u_3}
  [inst_2 : Ring R] [inst_3 : Module R G] (f : M → R) (g : M → G),
  fwdDiff h (f • g) = fwdDiff h f • g + f • fwdDiff h g + fwdDiff h f • fwdDiff h g
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.toKaroubi_obj_p : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  ((CategoryTheory.Idempotents.toKaroubi C).obj X).p = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Ring.Pi
/-- **Alias** of `NonUnitalRingHom.pi`.

---

A family of non-unital ring homomorphisms `f a : γ →ₙ+* β a` defines a non-unital ring
homomorphism `NonUnitalRingHom.pi f : γ →+* Π a, β a` given by
`NonUnitalRingHom.pi f x b = f b x`.  -/
Pi.nonUnitalRingHom : {I : Type u} →
  {f : I → Type u_1} →
    {γ : Type u_2} →
      [inst : (i : I) → NonUnitalNonAssocSemiring (f i)] →
        [inst_1 : NonUnitalNonAssocSemiring γ] → ((i : I) → γ →ₙ+* f i) → γ →ₙ+* (i : I) → f i
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.erase_monomial : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} {a : R}, Polynomial.erase n ((Polynomial.monomial n) a) = 0
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonWaitForDiagnosticsParams : Lean.ToJson Lean.Lsp.WaitForDiagnosticsParams
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.toDeleteEdges : ∀ {V : Type u} (G : SimpleGraph V) {v : V} (s : Set (Sym2 V)) {p : G.Walk v v},
  p.IsCycle → ∀ (hp : ∀ e ∈ p.edges, e ∉ s), (SimpleGraph.Walk.toDeleteEdges s p hp).IsCycle
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.liftFromUnderComp.match_1.eq_2 : ∀ {J : Type u_1} (motive : CategoryTheory.WithInitial J → Sort u_2) (a : J)
  (h_1 : Unit → motive CategoryTheory.WithInitial.star) (h_2 : (a : J) → motive (CategoryTheory.WithInitial.of a)),
  (match CategoryTheory.WithInitial.of a with
    | CategoryTheory.WithInitial.star => h_1 ()
    | CategoryTheory.WithInitial.of a => h_2 a) =
    h_2 a
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseWeekdayLong : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Weekday
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.equiv'_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (g : Polynomial R)
  (pb : PowerBasis R S) (h₁ : (Polynomial.aeval (AdjoinRoot.root g)) (minpoly R pb.gen) = 0)
  (h₂ : (Polynomial.aeval pb.gen) g = 0),
  ⇑(AdjoinRoot.equiv' g pb h₁ h₂) = ⇑(AdjoinRoot.liftAlgHom g (Algebra.ofId R S) pb.gen h₂)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.nullHomotopic_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0)
  (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ =
    CategoryTheory.CategoryStruct.comp h₁ S₂.f + CategoryTheory.CategoryStruct.comp S₁.g h₂
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.FGModuleCatDual_obj : ∀ (K : Type u) [inst : Field K] (V : FGModuleCat K),
  (FGModuleCat.FGModuleCatDual K V).obj = ModuleCat.of K (Module.Dual K ↑V)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.diag A))
  [inst_2 : CategoryTheory.Limits.HasInitial C] [HomotopicalAlgebra.IsCofibrant A]
  [(HomotopicalAlgebra.cofibrations C).IsStableUnderComposition],
  HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.PathObject.ofFactorizationData h).P
-- Init.Data.Array.MapIdx
Array.exists_of_mem_mapIdx : ∀ {β : Type u_1} {α : Type u_2} {f : ℕ → α → β} {b : β} {xs : Array α},
  b ∈ Array.mapIdx f xs → ∃ i, ∃ (h : i < xs.size), f i xs[i] = b
-- Lean.LoadDynlib
_private.Lean.LoadDynlib.0.Lean.Dynlib.SymbolImpl : Lean.Dynlib → NonemptyType
-- Lean.Meta.Transform
_private.Lean.Meta.Transform.0.Lean.Meta.transformWithCache.visit : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        (Lean.Expr → m Lean.TransformStep) →
          (Lean.Expr → m Lean.TransformStep) →
            Bool →
              Bool →
                Bool →
                  (x : STWorld IO.RealWorld m) →
                    MonadLiftT (ST IO.RealWorld) m →
                      Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr
-- Mathlib.Analysis.Convex.Function
ConcaveOn.convex_strict_hypograph : ∀ {𝕜 : 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 β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β} [ZeroLEOneClass 𝕜],
  ConcaveOn 𝕜 s f → Convex 𝕜 {p | p.1 ∈ s ∧ p.2 < f p.1}
-- Mathlib.Algebra.Module.LocalizedModule.Away
IsLocalizedModule.Away.exists_of_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N} (r : R)
  [IsLocalizedModule.Away r f] {x y : M}, f x = f y → ∃ n, r ^ n • x = r ^ n • y
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The composition of left adjoint mates is the adjoint mate of the composition.  -/
CategoryTheory.comp_leftAdjointMate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y]
  [inst_4 : CategoryTheory.HasLeftDual Z] {f : X ⟶ Y} {g : Y ⟶ Z},
  (ᘁCategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (ᘁg) (ᘁf)
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The underlying morphism of the inverse component of the right unitor isomorphism.  -/
Bimod.RightUnitorBimod.inv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        {R S : CategoryTheory.Mon C} → (P : Bimod R S) → P.X ⟶ Bimod.TensorBimod.X P (Bimod.regular S)
-- Mathlib.Algebra.Group.Commute.Units
Units.leftOfMul.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (a b : M) (hu : a * b = ↑u) (hc : Commute a b),
  u.leftOfMul a b hu hc = { val := a, inv := b * ↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOnFilter.mono_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' p'' : Filter α}, TendstoUniformlyOnFilter F f p p' → p'' ≤ p' → TendstoUniformlyOnFilter F f p p''
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.mk : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {s : Set E},
  (∀ x ∈ s, (p x 0).curry0 = f x) →
    (∀ (m : ℕ), ↑m < n → ∀ x ∈ s, HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft s x) →
      (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => p x m) s) → HasFTaylorSeriesUpToOn n f p s
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulRightStrictMono.toMulPosReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulRightReflectLE α], MulPosReflectLE α
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries.map : ∀ {G : Type u_1} [inst : AddGroup G] {K : Type u_2} [inst_1 : AddGroup K] (f : G →+ K) (n : ℕ),
  AddSubgroup.map f (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n
-- Init.Control.ExceptCps
/-- Use a monadic action that may throw an exception as an action that may return an exception's value.
 -/
ExceptCpsT.run : {m : Type u → Type u_1} → {ε α : Type u} → [Monad m] → ExceptCpsT ε m α → m (Except ε α)
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.biprodIsoProd_inv_comp_desc_apply : ∀ {G H K : AddCommGrpCat} (f : G ⟶ K) (g : H ⟶ K) (x : ↑G × ↑H),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.biprod.desc f g))
      ((CategoryTheory.ConcreteCategory.hom (G.biprodIsoProd H).inv) x) =
    (AddCommGrpCat.Hom.hom f) x.1 + (AddCommGrpCat.Hom.hom g) x.2
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The functor that exhibits `SimplexCategory` as skeleton
of `NonemptyFinLinOrd`  -/
SimplexCategory.skeletalFunctor : CategoryTheory.Functor SimplexCategory NonemptyFinLinOrd
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos_real : ∀ᶠ (x : ℝ) in Filter.atTop, 0 < 1 - AkraBazziRecurrence.smoothingFn x
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRoiIterIteratorOfUpwardEnumerableOfLeast? : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → [Std.PRange.Least? α] → Std.ToStream (Std.Roi α) (Std.Iter α)
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.card_left : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {S : Set G},
  AddSubgroup.IsComplement S ↑H → Nat.card ↑S = H.index
-- Mathlib.Algebra.Group.Ideal
/-- A semigroup ideal is finitely generated if it is generated by a finite set.

This is defeq to `SubMulAction.FG`, but unfolds more nicely.  -/
SemigroupIdeal.FG : {M : Type u_1} → [inst : Mul M] → SemigroupIdeal M → Prop
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.exists_app_map_eq_map_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {i : I} {U : (D.obj i).Opens},
  IsCompact ↑U →
    ∀ (s t : ↑((D.obj i).presheaf.obj (Opposite.op U))),
      (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (c.π.app i) U)) s =
          (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (c.π.app i) U)) t →
        ∃ j f,
          (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (D.map f) U)) s =
            (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (D.map f) U)) t
-- Mathlib.Data.Ordmap.Ordnode
BinaryTree.toOrdNode.eq_def : ∀ {α : Type u_1} (x : BinaryTree α),
  x.toOrdNode =
    match x with
    | BinaryTree.nil => Ordnode.nil
    | BinaryTree.node x l r => l.toOrdNode.node' x r.toOrdNode
-- Mathlib.Data.List.Forall2
List.forall₂_iff_get : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ : List α} {l₂ : List β},
  List.Forall₂ R l₁ l₂ ↔
    l₁.length = l₂.length ∧ ∀ (i : ℕ) (h₁ : i < l₁.length) (h₂ : i < l₂.length), R (l₁.get ⟨i, h₁⟩) (l₂.get ⟨i, h₂⟩)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.restrict_presheaf_obj : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (X_1 : (TopologicalSpace.Opens ↑U)ᵒᵖ),
  (X.restrict h).presheaf.obj X_1 = X.presheaf.obj (Opposite.op (h.functor.obj (Opposite.unop X_1)))
-- Mathlib.Logic.Equiv.Set
Equiv.image_monotone : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {e : α ≃ β} (s : Set α),
  Monotone ⇑e → Monotone ⇑(e.image s)
-- Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
LinearMap.clmOfExistsBoundedImage_coe : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E]
  [inst_2 : IsTopologicalAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : TopologicalSpace F]
  [inst_5 : NontriviallyNormedField 𝕜] [inst_6 : Module 𝕜 E] [inst_7 : ContinuousSMul 𝕜 E] [inst_8 : NormedField 𝕜']
  [inst_9 : Module 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_10 : RingHomIsometric σ] [inst_11 : IsTopologicalAddGroup F]
  {f : E →ₛₗ[σ] F} {h : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V)}, ↑(f.clmOfExistsBoundedImage h) = f
-- Lean.Environment
/-- Data computed once per extension for all three olean levels. Avoids calling the export function
three separate times so that expensive computations can be shared.  -/
Lean.OLeanEntries : Type → Type
-- Mathlib.Data.Set.Image
/-- If the only elements outside `s` are those left fixed by `σ`, then mapping by `σ` has no effect.
 -/
Set.image_perm : ∀ {α : Type u_1} {s : Set α} {σ : Equiv.Perm α}, {a | σ a ≠ a} ⊆ s → ⇑σ '' s = s
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `inter!` which can be used in the absence of balance
information but still assumes the preconditions of `filter`, otherwise might panic.  -/
Std.DTreeMap.Internal.Impl.inter! : {α : Type u} →
  {β : α → Type v} →
    [Ord α] → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Lean.Meta.Instances
Lean.Meta.getErasedInstances : Lean.CoreM (Lean.PHashSet Lean.Name)