mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.measurableSet_cut : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (r : α → β → Prop) (f : MeasureTheory.SimpleFunc α β),
  (∀ (b : β), MeasurableSet {a | r a b}) → MeasurableSet {a | r a (f a)}
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_some_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, t.get? k = some k' ↔ ∃ (h : k ∈ t), t.get k h = k'
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.pos_eq_endPos : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it → (it.i = it.s.rawEndPos ↔ r = [])
-- Mathlib.Order.BourbakiWitt
CompleteLattice.ωScottContinuous.sup : ∀ {α : Type u_1} {β : Type u_2} [inst : OmegaCompletePartialOrder α] [inst_1 : CompleteLattice β] {f g : α → β},
  OmegaCompletePartialOrder.ωScottContinuous f →
    OmegaCompletePartialOrder.ωScottContinuous g → OmegaCompletePartialOrder.ωScottContinuous (f ⊔ g)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  [self : P.IsStableUnderComposition] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  P f → P g → P (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.hasLineDerivWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₀ f₁ : E → F}
  {f' : F} {s : Set E} {x v : E},
  f₀ =ᶠ[nhdsWithin x s] f₁ → f₀ x = f₁ x → (HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_self : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M) (H : x ∈ S), f.mk' x ⟨x, H⟩ = 1
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_injective : ∀ {α : Type u_1}, Function.Injective Matroid.dual
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.rightUnitor_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable] (x : CategoryTheory.WideSubcategory P),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor x =
    CategoryTheory.WideSubcategory.isoMk (CategoryTheory.MonoidalCategoryStruct.rightUnitor x.obj) ⋯ ⋯
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateAltCodeImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Alt pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Alt pu
-- Init.Data.UInt.Lemmas
USize.sub_eq_add_neg : ∀ (a b : USize), a - b = a + -b
-- Mathlib.Analysis.Convex.Strong
UniformConvexOn.add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {f g : E → ℝ},
  UniformConvexOn s φ f → UniformConvexOn s ψ g → UniformConvexOn s (φ + ψ) (f + g)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an `AddZeroClass`, if it admits an
injective map that preserves `0` and `+` to an `AddZeroClass`.  -/
Function.Injective.addZeroClass : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : AddZeroClass M₂] →
          (f : M₁ → M₂) → Function.Injective f → f 0 = 0 → (∀ (x y : M₁), f (x + y) = f x + f y) → AddZeroClass M₁
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.coe_prod : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {H : Type u_2} [inst_2 : Group H]
  [inst_3 : TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H), ↑(U.prod V) = ↑U ×ˢ ↑V
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Bool
-- Mathlib.Algebra.DualNumber
/-- A ring morphism `R[ε] →+* R'` is determined by its restriction
on `R` and its value on `ε`.  -/
DualNumber.ringHom_ext : ∀ {R : Type u_1} [inst : CommSemiring R] {R' : Type u_5} [inst_1 : CommSemiring R'] {f g : DualNumber R →+* R'},
  f.comp (algebraMap R (DualNumber R)) = g.comp (algebraMap R (DualNumber R)) →
    f DualNumber.eps = g DualNumber.eps → f = g
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.mk : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] → [inst_3 : Coalgebra R A] → (val : A) → IsGroupLikeElem R val → GroupLike R A
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map₂_comm : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (xs ys : List.Vector α n) (f : α → α → β),
  (∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁) → List.Vector.map₂ f xs ys = List.Vector.map₂ f ys xs
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algebraMapInv.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  SymmetricAlgebra.algebraMapInv = SymmetricAlgebra.lift 0
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.forget₂_coalgebra_obj : ∀ {R : Type u} [inst : CommRing R] (X : BialgCat R),
  (CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).obj X = CoalgCat.of R X.carrier
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.support_mem_nhds : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E], Function.support ↑f ∈ nhds c
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.range_dualMap_le_dualAnnihilator_ker : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ →ₗ[R] M₂),
  f.dualMap.range ≤ f.ker.dualAnnihilator
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- This is another version of `gramSchmidt_orthogonal` using `Pairwise` instead.  -/
InnerProductSpace.gramSchmidt_pairwise_orthogonal : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E),
  Pairwise fun a b => inner 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f a) (InnerProductSpace.gramSchmidt 𝕜 f b) = 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.isLocalizationMap_id : ∀ {G : Type u_2} [inst : CommGroup G] (S : Submonoid G), S.IsLocalizationMap id
-- Init.Data.Array.Perm
Array.Perm.trans : ∀ {α : Type u_1} {xs ys zs : Array α}, xs.Perm ys → ys.Perm zs → xs.Perm zs
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
/-- `zeroAtFilterAddSubmonoid l` is the additive submonoid of `f : α → β`
which tend to zero along `l`.  -/
Filter.zeroAtFilterAddSubmonoid : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace β] → [inst_1 : AddZeroClass β] → [ContinuousAdd β] → Filter α → AddSubmonoid (α → β)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.QuaternionGroup.fintypeHelper : {n : ℕ} → ZMod (2 * n) ⊕ ZMod (2 * n) ≃ QuaternionGroup n
-- Mathlib.Tactic.NormNum.Inv
/-- The `norm_num` extension which identifies an expression `RatCast.ratCast q` where `norm_num`
recognizes `q`, returning the cast of `q`.  -/
Mathlib.Meta.NormNum.evalRatCast : Mathlib.Meta.NormNum.NormNumExt
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqvAux.match_1.eq_1 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) (x : 0 ≤ xs.size)
  (h_1 : (x : 0 ≤ xs.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
ContDiffWithinAt.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {n : ℕ∞},
  ContDiffWithinAt ℝ (↑n) f s x → ContDiffWithinAt ℝ (↑n) (fun x => Real.arctan (f x)) s x
-- Mathlib.Algebra.Order.Interval.Basic
Interval.divisionCommMonoid : {α : Type u_2} →
  [inst : CommGroup α] → [inst_1 : PartialOrder α] → [IsOrderedMonoid α] → DivisionCommMonoid (Interval α)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindex_refl : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), b.reindex (Equiv.refl ι) = b
-- Mathlib.Order.InitialSeg
InitialSeg.instEmbeddingLike : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, EmbeddingLike (InitialSeg r s) α β
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
ModuleCat.MonoidalCategory.braiding_inv_apply : ∀ {R : Type u} [inst : CommRing R] {M N : ModuleCat R} (m : ↑M) (n : ↑N),
  (CategoryTheory.ConcreteCategory.hom (β_ M N).inv) (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.HasPullback.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.Limits.HasPullback f g = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_prod_assoc : ∀ {𝕜 : 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'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞}, ContMDiff ((I.prod I').prod J) (I.prod (I'.prod J)) n fun x => (x.1.1, x.1.2, x.2)
-- Lean.Data.JsonRpc
Lean.JsonRpc.ResponseError.mk.injEq : ∀ {α : Type u} (id : Lean.JsonRpc.RequestID) (code : Lean.JsonRpc.ErrorCode) (message : String) (data? : Option α)
  (id_1 : Lean.JsonRpc.RequestID) (code_1 : Lean.JsonRpc.ErrorCode) (message_1 : String) (data?_1 : Option α),
  ({ id := id, code := code, message := message, data? := data? } =
      { id := id_1, code := code_1, message := message_1, data? := data?_1 }) =
    (id = id_1 ∧ code = code_1 ∧ message = message_1 ∧ data? = data?_1)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.coe_mk : ∀ (f : ℝ →o ℝ) (h : ∀ (x : ℝ), f.toFun (x + 1) = f.toFun x + 1), ⇑{ toOrderHom := f, map_add_one' := h } = ⇑f
-- Mathlib.Order.Interval.Finset.Defs
/-- A constructor from a definition of `Finset.Icc` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrder.ofIcc'`, this one requires `PartialOrder` but only
`DecidableEq`.  -/
LocallyFiniteOrder.ofIcc : (α : Type u_1) →
  [inst : PartialOrder α] →
    [DecidableEq α] →
      (finsetIcc : α → α → Finset α) → (∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) → LocallyFiniteOrder α
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univUnitBall_symm_apply : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (y : E),
  ↑OpenPartialHomeomorph.univUnitBall.symm y = (√(1 - ‖y‖ ^ 2))⁻¹ • y
-- Mathlib.CategoryTheory.PathCategory.Basic
/-- The functor from the canonical quotient of a path category of a category
to the original category.  -/
CategoryTheory.quotientPathsTo : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor (CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)) C
-- Lean.Widget.Types
/-- A JS [module](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
intended for use in user widgets.

The JS environment in which modules execute
provides a fixed set of libraries accessible via direct `import`,
notably [`@leanprover/infoview`](https://www.npmjs.com/package/@leanprover/infoview)
and [`react`](https://www.npmjs.com/package/react).

To initialize this field from an external JS file,
you may use `include_str "path"/"to"/"file.js"`.
However **beware** that this does not register a dependency with Lake,
so your Lean module will not automatically be rebuilt
when the `.js` file changes.  -/
Lean.Widget.Module.javascript : Lean.Widget.Module → String
-- Init.Data.AC
Lean.Data.AC.mergeIdem : List ℕ → List ℕ
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionContext.mk.injEq : ∀ (diagnostics : Array Lean.Lsp.Diagnostic) (only? : Option (Array Lean.Lsp.CodeActionKind))
  (triggerKind? : Option Lean.Lsp.CodeActionTriggerKind) (diagnostics_1 : Array Lean.Lsp.Diagnostic)
  (only?_1 : Option (Array Lean.Lsp.CodeActionKind)) (triggerKind?_1 : Option Lean.Lsp.CodeActionTriggerKind),
  ({ diagnostics := diagnostics, only? := only?, triggerKind? := triggerKind? } =
      { diagnostics := diagnostics_1, only? := only?_1, triggerKind? := triggerKind?_1 }) =
    (diagnostics = diagnostics_1 ∧ only? = only?_1 ∧ triggerKind? = triggerKind?_1)
-- Mathlib.MeasureTheory.Group.AEStabilizer
AddAction.aestabilizer_univ : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.VAddInvariantMeasure G α μ],
  AddAction.aestabilizer G μ Set.univ = ⊤
-- Lean.Meta.Basic
/-- Return `true` if `declName` is an inductive predicate. That is, `inductive` type in `Prop`.  -/
Lean.Meta.isInductivePredicate : Lean.Name → Lean.MetaM Bool
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_succ_right_eq_append : ∀ {m n : ℤ}, m < n → (m<...n + 1).toList = (m<...n).toList ++ [n]
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.cof_eq_cardinalMk : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [IsRegularCardinalOrder α],
  Order.cof α = Cardinal.mk α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_diff_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β k},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff m₂ ⋯).getD k fallback = m₁.getD k fallback
-- Mathlib.RingTheory.Ideal.Operations
/-- If `I` divides `J`, then `I` contains `J`.

In a Dedekind domain, to divide and contain are equivalent, see `Ideal.dvd_iff_le`.
 -/
Ideal.le_of_dvd : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, I ∣ J → J ≤ I
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.symm_symm : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.PartialEquiv M N), f.symm.symm = f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_sqrt_two : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A), autoParam (0 ≤ a) CFC.nnrpow_sqrt_two._auto_1 → CFC.sqrt a ^ 2 = a
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.funUnique_apply : ∀ (ι : Type u_4) (α : Type u_5) [inst : Unique ι] [inst_1 : UniformSpace α],
  ⇑(UniformEquiv.funUnique ι α) = fun f => f default
-- Mathlib.Algebra.Group.Hom.Defs
/-- `MonoidHom` down-cast to a `OneHom`, forgetting the multiplicative property.  -/
MonoidHom.coeToOneHom : {M : Type u_4} → {N : Type u_5} → [inst : MulOne M] → [inst_1 : MulOne N] → Coe (M →* N) (OneHom M N)
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.toNorm : {α : Type u_5} → [self : NormedField α] → Norm α
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsPreimmersion f],
  IsClosed (Set.range ⇑f) → AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.Order.BoundedOrder.Basic
lt_top_iff_ne_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a < ⊤ ↔ a ≠ ⊤
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.eq_of_eqOn_dense : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : Monoid M] {s : Set G},
  Subgroup.closure s = ⊤ → ∀ {f g : G →* M}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.Analysis.Matrix.LDL
_private.Mathlib.Analysis.Matrix.LDL.0.«term⟪_,_⟫ₑ» : Lean.ParserDescr
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_union_closure_left_eq : ∀ {α : Type u_2} (M : Matroid α) (X Y : Set α), M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_erase_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h : t.WF) {k : α},
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl k = default
-- Init.Prelude
BEq.mk : {α : Type u} → (α → α → Bool) → BEq α
-- Mathlib.Algebra.Polynomial.Basic
/-- **Alias** of `Polynomial.addSubmonoid_closure_setOfPred_eq_monomial`.

---

Monomials generate the additive monoid of polynomials.  -/
Polynomial.addSubmonoid_closure_setOf_eq_monomial : ∀ {R : Type u} [inst : Semiring R], AddSubmonoid.closure {p | ∃ n a, p = (Polynomial.monomial n) a} = ⊤
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_le : ∀ {f : ℝ → ℝ} {b : ℝ},
  b ∈ Set.Ioo 0 1 →
    AkraBazziRecurrence.GrowsPolynomially f →
      ∃ c > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The forgetful functor from the category of coalgebras, forgetting the coalgebraic structure.  -/
CategoryTheory.Endofunctor.Coalgebra.forget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C C) → CategoryTheory.Functor (CategoryTheory.Endofunctor.Coalgebra F) C
-- Lean.Meta.Tactic.Simp.Main
/-- Return true if `declName` is the name of a definition of the form
```
def declName ... :=
  match ... with
  | ...
```
 -/
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.isMatchDef : Lean.Name → Lean.CoreM Bool
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.evalAt_apply : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G] (g : G)
  (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤),
  ((LeftInvariantDerivation.evalAt g) X) f = (X f) g
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp_one : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  (f : R' →+* R''), MulChar.ringHomComp 1 f = 1
-- Init.Data.Sum.Lemmas
Sum.inl_getLeft : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β) (h : x.isLeft = true), Sum.inl (x.getLeft h) = x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.foldlM_eq_foldlM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.DTreeMap.Raw.foldlM f init t = List.foldlM (fun a b => f a b.1 b.2) init (Std.DTreeMap.Raw.Const.toList t)
-- Mathlib.MeasureTheory.PiSystem
generateFrom_measurableSet_of_generatePiSystem : ∀ {α : Type u_1} {g : Set (Set α)}, ∀ t ∈ generatePiSystem g, MeasurableSet t
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- `CNF.coeff b o` is the finitely supported function returning the coefficient of `b ^ e` in the
Cantor Normal Form (`CNF`) of `o`, for each `e`.  -/
Ordinal.CNF.coeff : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1} →₀ Ordinal.{u_1}
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.pushAnchor : Lean.Meta.Grind.TAnchor✝ → Lean.Meta.Grind.Collector.Collect✝ Unit
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.map_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g) CategoryTheory.Limits.biprod.snd =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd g
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- If `G` acts isometrically on `X`, then the image of a bounded set in `X` under scalar
multiplication by `c : G` is bounded. See also `Bornology.IsBounded.smul₀` for a similar lemma about
normed spaces.  -/
Bornology.IsBounded.smul : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : SMul G X] [IsIsometricSMul G X] {s : Set X},
  Bornology.IsBounded s → ∀ (c : G), Bornology.IsBounded (c • s)
-- Mathlib.Algebra.Order.Sub.Basic
AddLECancellable.tsub_lt_self_iff : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, AddLECancellable a → (a - b < a ↔ 0 < a ∧ 0 < b)
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of the coordinate-wise `n`th power of a tuple
is the `n`th power of its multiplicative height.  -/
Height.mulHeight_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (n : ℕ),
  Height.mulHeight (x ^ n) = Height.mulHeight x ^ n
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Ico' : ∀ {α : Type u_1} [inst : LinearOrder α] {b c d : α}, c ≤ b → Set.Iio b ∪ Set.Ico c d = Set.Iio (max b d)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of the reverse direction of `Set.injective_codRestrict`. -/
Function.Injective.codRestrict : ∀ {α : Type u_1} {ι : Sort u_5} {f : ι → α} {s : Set α} (h : ∀ (x : ι), f x ∈ s),
  Function.Injective f → Function.Injective (Set.codRestrict f s h)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.LocallyLinear.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α),
  G.LocallyLinear = (G.EdgeDisjointTriangles ∧ ∀ ⦃x y : α⦄, G.Adj x y → ∃ s, G.IsNClique 3 s ∧ x ∈ s ∧ y ∈ s)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mk_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : Y ⟶ X), (CategoryTheory.Over.mk f).hom = f
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.le_opNorm_mul_pow_card_of_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F) {m : ι → E} {b : ℝ},
  ‖m‖ ≤ b → ‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_uIcc : ∀ {α : Type u_1} [inst : Lattice α] [LocallyFiniteOrder α] (a b : α), (Set.uIcc a b).Finite
-- Std.Http.Protocol.H1.Parser
/-- Parses fixed-size chunk data that can be incomplete.
 -/
Std.Http.Protocol.H1.parseChunkSizedData : ℕ → Std.Internal.Parsec.ByteArray.Parser Std.Http.Protocol.H1.TakeResult