mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Linter.Style
/-- The `nameCheck` linter emits a warning on declarations whose name is non-standard style.
(Currently, this only includes declarations whose name includes a double underscore.)

**Why is this bad?** Double underscores in theorem names can be considered non-standard style and
probably have been introduced by accident.
**How to fix this?** Use single underscores to separate parts of a name, following standard naming
conventions.
 -/
Mathlib.Linter.linter.style.nameCheck : Lean.Option Bool
-- Mathlib.CategoryTheory.ObjectProperty.Comma
CategoryTheory.ObjectProperty.instEssentiallySmallCommaCommaOfLocallySmall : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (F₁ : CategoryTheory.Functor C₁ D) (F₂ : CategoryTheory.Functor C₂ D) (P₁ : CategoryTheory.ObjectProperty C₁)
  (P₂ : CategoryTheory.ObjectProperty C₂) [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁]
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂] [CategoryTheory.LocallySmall.{w, v_3, u_3} D],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, max v_1 v_2, max (max u_1 u_2) v_3}
    (CategoryTheory.ObjectProperty.comma F₁ F₂ P₁ P₂)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- To show that an invariant σ-finite measure is regular it is sufficient to show that it is finite
on some compact set with non-empty interior.  -/
MeasureTheory.Measure.regular_of_isMulLeftInvariant : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] [SecondCountableTopology G] {μ : MeasureTheory.Measure G} [MeasureTheory.SigmaFinite μ]
  [μ.IsMulLeftInvariant] {K : Set G}, IsCompact K → (interior K).Nonempty → μ K ≠ ⊤ → μ.Regular
-- Init.Data.BitVec.Lemmas
BitVec.sle_iff_toInt_le : ∀ {w : ℕ} {x y : BitVec w}, x.sle y = true ↔ x.toInt ≤ y.toInt
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.of_precomp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {π : ι → Set (Set Ω)} {ι' : Type u_5} {g : ι' → ι},
  Function.Surjective g → ProbabilityTheory.Kernel.iIndepSets (π ∘ g) κ μ → ProbabilityTheory.Kernel.iIndepSets π κ μ
-- Init.Data.Option.Lemmas
Option.join_eq_get : ∀ {α : Type u_1} {x : Option (Option α)} {h : x.isSome = true}, x.join = x.get h
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- The extensive Grothendieck topology on a finitary pre-extensive category `C`.
 -/
CategoryTheory.extensiveTopology : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.FinitaryPreExtensive C] → CategoryTheory.GrothendieckTopology C
-- Mathlib.LinearAlgebra.Determinant
/-- If a linear map has determinant different from `1`, then the module is free.  -/
LinearMap.free_of_det_ne_one : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : M →ₗ[R] M},
  LinearMap.det f ≠ 1 → Module.Free R M
-- Mathlib.Analysis.Convex.Deriv
StrictMonoOn.exists_deriv_lt_slope : ∀ {x y : ℝ} {f : ℝ → ℝ},
  ContinuousOn f (Set.Icc x y) →
    x < y → StrictMonoOn (deriv f) (Set.Ioo x y) → ∃ a ∈ Set.Ioo x y, deriv f a < (f y - f x) / (y - x)
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.mapCochainComplexSingleFunctor.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {D : Type u'} [inst_3 : CategoryTheory.Category.{v', u'} D]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℤ),
  F.mapCochainComplexSingleFunctor n = HomologicalComplex.singleMapHomologicalComplex F (ComplexShape.up ℤ) n
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_one : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k], { coeff := fun₀ | 1 => 1 } = 1
-- Init.Grind.Ordered.Rat
Lean.Grind.instIsLinearOrderRat : Std.IsLinearOrder ℚ
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_0_comp_chainsIso₀_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : (Fin 0 → G) →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₀ B).hom)
      ((CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap f φ).f 0)) x) =
    (Rep.Hom.hom φ) ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₀ A).hom) x)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n + a = n') (γ : CochainComplex.HomComplex.Cochain K L n),
  (CochainComplex.HomComplex.Cochain.leftShiftAddEquiv K L n a n' hn') γ = γ.leftShift a n' hn'
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_ofBijective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {φ : P₁ →ᵃ[k] P₂} (hφ : Function.Bijective ⇑φ),
  (AffineEquiv.ofBijective hφ).linear = LinearEquiv.ofBijective φ.linear ⋯
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `dist (f n) (f (n+1))` is bounded by `(C / 2) / 2^n`, then `f` is a Cauchy sequence.  -/
cauchySeq_of_le_geometric_two : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {C : ℝ} {f : ℕ → α},
  (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) → CauchySeq f
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx (Lean.Grind.CommRing.Expr.num k) = OfNat.ofNat k.natAbs
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_ofObjects : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} (X : I → C) {Y Z : C} (f : Z ⟶ Y),
  CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.ofObjects X Y) = CategoryTheory.Sieve.ofObjects X Z
-- Init.Data.String.Lemmas.Order
String.Pos.sliceTo_le_sliceTo_iff : ∀ {s : String} {p₀ q r : s.Pos} {h₁ : q ≤ p₀} {h₂ : r ≤ p₀}, p₀.sliceTo q h₁ ≤ p₀.sliceTo r h₂ ↔ q ≤ r
-- Mathlib.Data.Int.Bitwise
/-- `lnot` flips all the bits in the binary representation of its input  -/
Int.lnot : ℤ → ℤ
-- Lean.Linter.Init
/-- Builtin linter sets registered from `builtin_initialize` blocks in core code.

Entries here are folded into every `LinterSetsState` produced by `linterSetsExt`, so they
participate in `getLinterValue` like any user-declared set.
 -/
Lean.Linter.builtinLinterSetsRef : IO.Ref (Array (Lean.Name × Lean.NameSet))
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.id_apply : ∀ {α : Type u_2} [inst : Min α] [inst_1 : Top α] (a : α), (InfTopHom.id α) a = a
-- Mathlib.Algebra.Module.Bimodule
Subbimodule.coe_toSubmodule' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M), ↑(Subbimodule.toSubmodule' p) = ↑p
-- Init.Data.String.Substring
Substring.Raw.Internal.takeWhileImpl : Substring.Raw → (Char → Bool) → Substring.Raw
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_compl : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α), ↑aᶜ = (↑a)ᶜ
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.leadingCoeff_le_mahlerMeasure : ∀ (p : Polynomial ℂ), ‖p.leadingCoeff‖ ≤ p.mahlerMeasure
-- Mathlib.Algebra.Ring.Action.Basic
/-- Compose a `MulSemiringAction` with a `MonoidHom`, with action `f r' • m`.
See note [reducible non-instances].  -/
MulSemiringAction.compHom : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] →
        (R : Type v) → [inst_2 : Semiring R] → (N →* M) → [MulSemiringAction M R] → MulSemiringAction N R
-- Mathlib.Order.Antichain
IsAntichain.of_strictMonoOn_antitoneOn : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → AntitoneOn f s → IsAntichain (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.RingTheory.Finiteness.Defs
/-- A module over a semiring is `Module.Finite` if it is finitely generated as a module.  -/
Module.Finite : (R : Type u_1) → (M : Type u_4) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- Preserving finite colimits also implies preserving colimits over finite shapes in higher
universes.
 -/
CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteColimits F] (J : Type w)
  [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.Data.Nat.PrimeFin
Nat.toFinset_factors : ∀ (n : ℕ), n.primeFactorsList.toFinset = n.primeFactors
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.congr_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι} {g : α → β},
  TendstoLocallyUniformly F f p → (∀ (x : α), f x = g x) → TendstoLocallyUniformly F g p
-- Init.Data.UInt.Lemmas
UInt16.ofFin_mk : ∀ {n : ℕ} (hn : n < UInt16.size), UInt16.ofFin ⟨n, hn⟩ = UInt16.ofNatLT n hn
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_le_iff_of_lt_aleph0 : ∀ {a : Cardinal.{u}} (n : ℕ), a < Cardinal.aleph0 → (Cardinal.toNat a ≤ n ↔ a ≤ ↑n)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.bracket_ofTwoCocycle : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {c : ↥(LieModule.Cohomology.twoCocycle R L M)} (x y : LieAlgebra.ofTwoCocycle c),
  ⁅x, y⁆ =
    (LieAlgebra.ofProd c)
      (⁅((LieAlgebra.ofProd c).symm x).1, ((LieAlgebra.ofProd c).symm y).1⁆,
        (↑↑c ((LieAlgebra.ofProd c).symm x).1) ((LieAlgebra.ofProd c).symm y).1 +
            ⁅((LieAlgebra.ofProd c).symm x).1, ((LieAlgebra.ofProd c).symm y).2⁆ -
          ⁅((LieAlgebra.ofProd c).symm y).1, ((LieAlgebra.ofProd c).symm x).2⁆)
-- Lean.Attributes
Lean.Attribute.Builtin.getId? : Lean.Syntax → Lean.AttrM (Option Lean.Name)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.ι_desc_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → B ⟶ objs j) [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f : B ⟶ X)
  (fs : (j : J) → objs j ⟶ X) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f) (j : J) {Z : C}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.ι arrows j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePushout.desc f fs w) h) =
    CategoryTheory.CategoryStruct.comp (fs j) h
-- Mathlib.Data.ZMod.Basic
/-- **Alias** of the reverse direction of `ZMod.natCast_eq_zero_iff_even`. -/
Even.natCast_zmod_two : ∀ {n : ℕ}, Even n → ↑n = 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.halt : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → Turing.TM1.Stmt Γ Λ σ
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.commSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommMonoid M],
  MonoidAlgebra.commSemiring = { toSemiring := MonoidAlgebra.semiring, mul_comm := ⋯ }
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.homeoOfIso_symm : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y),
  (AlgebraicGeometry.Scheme.homeoOfIso e).symm = AlgebraicGeometry.Scheme.homeoOfIso e.symm
-- Mathlib.Algebra.Order.Group.Synonym
toDual_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : β), OrderDual.toDual (a ^ b) = OrderDual.toDual a ^ b
-- Mathlib.Order.Circular
CircularPartialOrder.mk : {α : Type u_1} →
  [toCircularPreorder : CircularPreorder α] →
    (∀ {a b c : α}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a) → CircularPartialOrder α
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithTop.iSup_coe_eq_top : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
  ⨆ x, ↑(f x) = ⊤ ↔ ¬BddAbove (Set.range f)
-- Mathlib.Analysis.Analytic.Linear
analyticOn_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {t : Set (E × F)}, AnalyticOn 𝕜 (fun p => p.1) t
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instFaithfulSMulSubtypeMem : ∀ {M' : Type u_5} {α : Type u_6} [inst : SMul M' α] {S' : Type u_7} [inst_1 : SetLike S' M'] (s : S')
  [FaithfulSMul M' α], FaithfulSMul (↥s) α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.union_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∪ t₂).Equiv (t₃ ∪ t₄)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Two forks of the form `ofι` are isomorphic whenever their `ι`'s are equal.  -/
CategoryTheory.Limits.ForkOfι.ext : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {P : C} →
          {ι ι' : P ⟶ X} →
            (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) →
              (w' : CategoryTheory.CategoryStruct.comp ι' f = CategoryTheory.CategoryStruct.comp ι' g) →
                ι = ι' → (CategoryTheory.Limits.Fork.ofι ι w ≅ CategoryTheory.Limits.Fork.ofι ι' w')
-- Mathlib.Algebra.Order.Floor.Div
Pi.ceilDiv_apply : ∀ {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : (i : ι) → AddCommMonoid (π i)] [inst_3 : (i : ι) → PartialOrder (π i)]
  [inst_4 : (i : ι) → SMulZeroClass α (π i)] [inst_5 : (i : ι) → CeilDiv α (π i)] (f : (i : ι) → π i) (a : α) (i : ι),
  (f ⌈/⌉ a) i = f i ⌈/⌉ a
-- Mathlib.Logic.Equiv.Finset
Denumerable.raise'.eq_1 : ∀ (x : ℕ), Denumerable.raise' [] x = []
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.val_mulMap'_tmul : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S}
  (m : ↥M) (n : ↥N), ↑((M.mulMap' N) (m ⊗ₜ[R] n)) = ↑m * ↑n
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instDecidableEq : (R : Type u) → [inst : Semiring R] → [DecidableEq R] → DecidableEq (Polynomial R)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.graph.eq_1 : ∀ {L : FirstOrder.Language} {n : ℕ} (f : L.Functions n),
  FirstOrder.Language.Formula.graph f =
    (FirstOrder.Language.var 0).equal (FirstOrder.Language.func f fun i => FirstOrder.Language.var i.succ)
-- Init.Data.SInt.Lemmas
USize.ofBitVec_iSizeToBitVec : ∀ (x : ISize), { toBitVec := x.toBitVec } = x.toUSize
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C),
  ((t.triangleLTLTGELT a b h).obj j).obj₂ = (t.truncLT b).obj j
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns `true` if free variables in `type` are not in `thmVars` or are in `fvarsFound`.
We use this function to check whether `type` is fully instantiated.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.checkTypeFVars : Lean.FVarIdSet → Lean.FVarIdSet → Lean.Expr → Bool
-- Mathlib.Data.ULift
ULift.up_inj : ∀ {α : Type u} {x y : α}, { down := x } = { down := y } ↔ x = y
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_injective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Surjective ⇑f → Function.Injective (AddSubgroup.comap f)
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_mono : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s₁ s₂ : Multiset α}, s₁ ⊆ s₂ → s₂.inf ≤ s₁.inf
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.instHasInjectiveDimensionLTBiprod : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X Y : C) (n : ℕ)
  [CategoryTheory.HasInjectiveDimensionLT X n] [CategoryTheory.HasInjectiveDimensionLT Y n],
  CategoryTheory.HasInjectiveDimensionLT (X ⊞ Y) n
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- If two non-unital ring homomorphisms are equal on a set, then they are equal on its
non-unital subsemiring closure.  -/
NonUnitalRingHom.eqOn_sclosure : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [NonUnitalRingHomClass F R S] {f g : F} {s : Set R},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(NonUnitalSubsemiring.closure s)
-- Mathlib.Topology.Sion
_private.Mathlib.Topology.Sion.0.Sion.mem_sublevelLeft_iff : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β} {b : β}
  {y : ↑Y} {x : ↑X}, x ∈ Sion.sublevelLeft✝ X f b ↑y ↔ f ↑x ↑y ≤ b
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.CotangentSpace.span_image_eq_top_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R]
  {s : Set ↥(IsLocalRing.maximalIdeal R)},
  Submodule.span (IsLocalRing.ResidueField R) (⇑(IsLocalRing.maximalIdeal R).toCotangent '' s) = ⊤ ↔
    Submodule.span R s = ⊤
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `Over.map` commutes with composition.  -/
CategoryTheory.MorphismProperty.Over.mapComp : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          {X Y Z : T} →
            [inst_2 : P.IsStableUnderComposition] →
              {f : X ⟶ Y} →
                (hf : P f) →
                  {g : Y ⟶ Z} →
                    (hg : P g) →
                      [Q.RespectsIso] →
                        (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g)) →
                          (hfg :
                              autoParam (fg = CategoryTheory.CategoryStruct.comp f g)
                                CategoryTheory.MorphismProperty.Over.mapComp._auto_1) →
                            CategoryTheory.MorphismProperty.Over.map Q ⋯ ≅
                              (CategoryTheory.MorphismProperty.Over.map Q hf).comp
                                (CategoryTheory.MorphismProperty.Over.map Q hg)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_empty : ↑∅ = ∅
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries.eq_top`. -/
upperCentralSeries.eq_top : ∀ {G : Type u_1} [inst : Group G] [Group.IsNilpotent G] {a b : ℕ},
  a ≠ b → Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b → Subgroup.upperCentralSeries G a = ⊤
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
/-- The bicategory structure on `EnrichedCat V` for a monoidal category `V`.  -/
CategoryTheory.EnrichedCat.bicategory : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] → CategoryTheory.Bicategory (CategoryTheory.EnrichedCat V)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
/-- (Implementation detail, see `LinearMap.nilRank`.)

Let `L` and `M` be finite free modules over `R`,
and let `φ : L →ₗ[R] Module.End R M` be a linear family of endomorphisms.
Then `LinearMap.nilRankAux φ b` is the smallest index
at which `LinearMap.polyCharpoly φ b` has a non-zero coefficient.

This number does not depend on the choice of `b`, see `nilRankAux_basis_indep`.  -/
LinearMap.nilRankAux : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      {ι : Type u_5} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup L] →
            [inst_2 : Module R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [Fintype ι] →
                    [DecidableEq ι] →
                      [Module.Free R M] → [Module.Finite R M] → (L →ₗ[R] Module.End R M) → Module.Basis ι R L → ℕ
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.finite_minimalCover : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal}, (Metric.minimalCover ε A).Finite
-- Batteries.Data.Fin.Coding
Fin.encodeSum_decodeSum : ∀ {n m : ℕ} (x : Fin (n + m)), Fin.encodeSum (Fin.decodeSum x) = x
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.of_subsingleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [Subsingleton X] (f : X → Y),
  Topology.IsEmbedding f
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instZero : {ι : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] → {I₀ : WithTop (BoxIntegral.Box ι)} → Zero (BoxIntegral.BoxAdditiveMap ι M I₀)
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_succ_nil : ∀ {α : Type u} {n : ℕ} {a : α}, [].insertIdx (n + 1) a = []
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
VectorBundle.injective_eval_contMDiffAt_sec : ∀ {𝕜 : 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] (F : Type u_5) [inst_6 : NormedAddCommGroup F]
  (V : M → Type u_6) [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → AddCommGroup (V x)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  [inst_12 : (x : M) → Module 𝕜 (V x)] (W : Type u_7) [inst_13 : AddCommGroup W] [inst_14 : Module 𝕜 W]
  [inst_15 : TopologicalSpace W] (x : M), Function.Injective fun A Z x_1 => A (Z x)
-- Lean.Data.Name
_private.Lean.Data.Name.0.Lean.Name.quickCmpImpl.unsafe_impl_2 : Lean.Name → Lean.Name → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Congr
differentiableWithinAt_congr_set_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  s =ᶠ[nhdsWithin x {x}ᶜ] t → (DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- Composition of a continuous function vanishing at infinity with a cocompact map yields another
continuous function vanishing at infinity.  -/
ZeroAtInftyContinuousMap.comp : {β : Type v} →
  {γ : Type w} →
    {δ : Type u_2} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            [inst_3 : Zero δ] → ZeroAtInftyContinuousMap γ δ → CocompactMap β γ → ZeroAtInftyContinuousMap β δ