mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.hygieneInfoNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The machine states of the TM2 emulator. We can either be in a normal state when waiting for the
next TM2 action, or we can be in the "go" and "return" states to go to the top of the stack and
return to the bottom, respectively.  -/
Turing.TM2to1.Λ' : (K : Type u_1) → (K → Type u_2) → Type u_3 → Type u_4 → Type (max (max (max u_1 u_2) u_3) u_4)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instMulOneClass : {α : Type u_1} → [MulOneClass α] → MulOneClass (Colex α)
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.Q.mk : {α : Type u} → [inst : Lean.Grind.NatModule α] → α × α → Lean.Grind.IntModule.OfNatModule.Q α
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- `persistFVars` is one step in persisting: track a single `FVarId` between two `LocalContext`s.
If an `FVarId` with the same unique name exists in the new context, use it.
Otherwise, if an `FVarId` with the same `userName` exists in the new context, use it.
If both of these fail, return `default` (i.e. "fail").  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.persistFVars : Lean.FVarId → Lean.LocalContext → Lean.LocalContext → Lean.FVarId
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- The canonical map from the type to the free group is an injection.  -/
FreeGroup.of_injective : ∀ {α : Type u}, Function.Injective FreeGroup.of
-- Init.Data.List.Basic
List.getLastD_cons : ∀ {α : Type u} {a b : α} {l : List α}, (b :: l).getLastD a = l.getLastD b
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_mulRight : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [MeasurableMul G] (g : G),
  MeasurableEmbedding fun x => x * g
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- the underlying simplicial object  -/
CategoryTheory.SimplicialObject.Split.X : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.SimplicialObject.Split C → CategoryTheory.SimplicialObject C
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Int.trailingZeros.aux.match_1.eq_1 : ∀ (i : ℤ) (motive : (k : ℕ) → k ≠ 0 → i.natAbs ≤ k → Sort u_1) (k : ℕ) (x : k + 1 ≠ 0) (hk : i.natAbs ≤ k + 1)
  (h_1 : (k : ℕ) → (x : k + 1 ≠ 0) → (hk : i.natAbs ≤ k + 1) → motive k.succ x hk),
  (match k.succ, x, hk with
    | k.succ, x, hk => h_1 k x hk) =
    h_1 k x hk
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.prodEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D'),
  (CategoryTheory.CostructuredArrow.prodEquivalence S S' T T').inverse =
    CategoryTheory.CostructuredArrow.prodInverse S S' T T'
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₃₂_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G × G × G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₃₂ A)) fun₀ | g => a) =
    (((fun₀ | (g.2.1, g.2.2) => (A.ρ g.1⁻¹) a) - fun₀ | (g.1 * g.2.1, g.2.2) => a) + fun₀ | (g.1, g.2.1 * g.2.2) => a) -
      fun₀ | (g.1, g.2.1) => a
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.instIsStrictOrderedRing : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : Semiring β] [inst_1 : PartialOrder β] [IsStrictOrderedRing β],
  IsStrictOrderedRing ((↑φ).Germ β)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trCfg.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (motive : Turing.TM1.Cfg Γ Λ σ → Sort u_4)
  (l : Option Λ) (v : σ) (T : Turing.Tape Γ)
  (h_1 : (l : Option Λ) → (v : σ) → (T : Turing.Tape Γ) → motive { l := l, var := v, Tape := T }),
  (match { l := l, var := v, Tape := T } with
    | { l := l, var := v, Tape := T } => h_1 l v T) =
    h_1 l v T
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The canonical map `X ⟶ Spec Γ(X, ⊤)`. This is the unit of the `Γ-Spec` adjunction.  -/
AlgebraicGeometry.LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace : AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.Faithful
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.invEmbedding_comp : ∀ {n : ℕ} (c : Composition n) (i : Fin c.length) (j : Fin (c.blocksFun i)), ↑(c.invEmbedding ((c.embedding i) j)) = ↑j
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a ring homomorphism `f`, the induced homomorphism
on the quotient by `f`'s kernel has the same image as `f`.  -/
RingCon.kerLift_range_eq : ∀ {M : Type u_1} {P : Type u_3} [inst : Ring M] [inst_1 : Ring P] {f : M →+* P}, (RingCon.kerLift f).range = f.range
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofHom_id : ∀ {X : Type u} [inst : AddGroup X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalAddGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X],
  ProfiniteAddGrp.ofHom (ContinuousAddMonoidHom.id X) = CategoryTheory.CategoryStruct.id (ProfiniteAddGrp.of X)
-- Lean.Parser.Command
Lean.Parser.Command.openRenaming.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Height
Set.chainHeight_empty : ∀ {α : Type u_1} (r : α → α → Prop), ∅.chainHeight r = 0
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.fromGeneratedByTopCat_map_hom_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {X_1 Y : GeneratedByTopCat X} (f : X_1 ⟶ Y)
  (a : ↑X_1.obj),
  (ContinuousGeneratedByCat.fromGeneratedByTopCat.map f).hom a = (CategoryTheory.ConcreteCategory.hom f) a
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.kunion.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List (Sigma β) → List (Sigma β) → Sort u_3) (l₂ : List (Sigma β))
  (h_1 : (l₂ : List (Sigma β)) → motive [] l₂)
  (h_2 : (s : Sigma β) → (l₁ : List (Sigma β)) → (l₂ : List (Sigma β)) → motive (s :: l₁) l₂),
  (match [], l₂ with
    | [], l₂ => h_1 l₂
    | s :: l₁, l₂ => h_2 s l₁ l₂) =
    h_1 l₂
-- Mathlib.Order.Closure
ClosureOperator.closure_iSup_closure : ∀ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (c : ClosureOperator α) (f : ι → α),
  c (⨆ i, c (f i)) = c (⨆ i, f i)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.instMonoid : {ι : Type u_1} →
  {A : Type u_2} → {σ : Type u_6} → [inst : Semiring A] → [inst_1 : SetLike σ A] → {𝒜 : ι → σ} → Monoid (𝒜 →+*ᵍ 𝒜)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
/-- See also `continuousAt_cpow` for a version that assumes `p.1 ≠ 0` but makes no
assumptions about `p.2`.  -/
Complex.continuousAt_cpow_of_re_pos : ∀ {p : ℂ × ℂ}, 0 ≤ p.1.re ∨ p.1.im ≠ 0 → 0 < p.2.re → ContinuousAt (fun x => x.1 ^ x.2) p
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_empty : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω), μ[|∅] = 0
-- Mathlib.Topology.Category.TopCat.ULift
TopCat.uliftFunctorObjHomeo_symm_naturality_apply : ∀ {X Y : TopCat} (f : X ⟶ Y) (x : ↑(TopCat.uliftFunctor.obj X)),
  Y.uliftFunctorObjHomeo.symm ((CategoryTheory.ConcreteCategory.hom (TopCat.uliftFunctor.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom f) (X.uliftFunctorObjHomeo.symm x)
-- Mathlib.Tactic.DefEqTransformations
/-- `eta_expand at loc` eta expands all sub-expressions at the given location.
It also beta reduces any applications of eta expanded terms, so it puts it
into an eta-expanded "normal form."
This also exists as a `conv`-mode tactic.

For example, if `f` takes two arguments, then `f` becomes `fun x y => f x y`
and `f x` becomes `fun y => f x y`.

This can be useful to turn, for example, a raw `HAdd.hAdd` into `fun x y => x + y`.
 -/
Mathlib.Tactic.etaExpandStx : Lean.ParserDescr
-- Lean.Meta.Coe
/-- Coerces `expr` to a function type.  -/
Lean.Meta.coerceToFunction? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.reverse.go : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Init.Data.SInt.Lemmas
Int8.mod_zero : ∀ {a : Int8}, a % 0 = a
-- Mathlib.Algebra.Ring.Defs
NonUnitalSemiring.toSemigroupWithZero : {α : Type u} → [self : NonUnitalSemiring α] → SemigroupWithZero α
-- Lean.Meta.Basic
Lean.Meta.FunInfo.mk.sizeOf_spec : ∀ (paramInfo : Array Lean.Meta.ParamInfo) (resultDeps : Array ℕ),
  sizeOf { paramInfo := paramInfo, resultDeps := resultDeps } = 1 + sizeOf paramInfo + sizeOf resultDeps
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.eq_1 : ∀ (K : Type u_1) [inst : Field K], NumberField.canonicalEmbedding K = RingHom.pi fun φ => φ
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.ext_hom_iff : ∀ {α : Type u} {M : Type u_1} [inst : AddMonoid M] {f g : FreeAddGroup α →+ M},
  f = g ↔ ∀ (a : α), f (FreeAddGroup.of a) = g (FreeAddGroup.of a)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsLittleO.add_isTheta : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {l : Filter α}
  {f₁ f₂ : α → E'} {g : α → F}, f₁ =o[l] g → f₂ =Θ[l] g → (f₁ + f₂) =Θ[l] g
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!_eq_foldl : ∀ {α : Type u} {x : Ord α} {l : List α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) =
    List.foldl (fun acc k => Std.DTreeMap.Internal.Impl.insertIfNew! k () acc) t l
-- Mathlib.Data.Nat.Nth
Nat.nth_le_nth' : ∀ {p : ℕ → Prop} {m n : ℕ}, m ≤ n → (∀ (hf : (Set.ofPred p).Finite), n < hf.toFinset.card) → Nat.nth p m ≤ Nat.nth p n
-- Mathlib.Data.Multiset.Defs
Multiset.Subset.trans : ∀ {α : Type u_1} {s t u : Multiset α}, s ⊆ t → t ⊆ u → s ⊆ u
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.ncard_block_eq_relIndex : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [AddAction.IsPretransitive G X]
  {B : Set X},
  AddAction.IsBlock G B → ∀ {x : X}, x ∈ B → B.ncard = (AddAction.stabilizer G x).relIndex (AddAction.stabilizer G B)
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toBitVec = BitVec.ofNat 8 n
-- Init.Grind.Norm
Lean.Grind.Nat.lt_eq : ∀ (a b : ℕ), (a < b) = (a + 1 ≤ b)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
/-- A measure `μ` is called a probability measure if `μ univ = 1`.  -/
MeasureTheory.IsProbabilityMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.Analysis.Normed.Field.Basic
/-- A nontrivially normed field is a normed field in which there is an element of norm different
from `0` and `1`. This makes it possible to bring any element arbitrarily close to `0` by
multiplication by the powers of any element, and thus to relate algebra and topology.  -/
NontriviallyNormedField : Type u_5 → Type u_5
-- Mathlib.Topology.Instances.Nat
Nat.pairwise_one_le_dist : Pairwise fun m n => 1 ≤ dist m n
-- Init.Data.String.Basic
String.Slice.isUTF8FirstByte_utf8ByteAt_zero : ∀ {s : String.Slice} {h : 0 < s.rawEndPos}, (s.getUTF8Byte 0 h).IsUTF8FirstByte
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `HasMFDerivAt I I' f x f'` indicates that the function `f` between manifolds
has, at the point `x`, the derivative `f'`. Here, `f'` is a continuous linear
map from the tangent space at `x` to the tangent space at `f x`.

We require continuity in the definition, as otherwise points close to `x` in `s` could be sent by
`f` outside of the chart domain around `f x`. Then the chart could do anything to the image points,
and in particular by coincidence `writtenInExtChartAt I I' x f` could be differentiable, while
this would not mean anything relevant.  -/
HasMFDerivAt : {𝕜 : 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 : M → M') → (x : M) → (TangentSpace I x →L[𝕜] TangentSpace I' (f x)) → Prop
-- Init.Prelude
Fin.decLt : {n : ℕ} → (a b : Fin n) → Decidable (a < b)
-- Aesop.Options.Internal
Aesop.Options'.mk.injEq : ∀ (toOptions : Aesop.Options) (generateScript : Bool) (forwardMaxDepth? : Option ℕ) (toOptions_1 : Aesop.Options)
  (generateScript_1 : Bool) (forwardMaxDepth?_1 : Option ℕ),
  ({ toOptions := toOptions, generateScript := generateScript, forwardMaxDepth? := forwardMaxDepth? } =
      { toOptions := toOptions_1, generateScript := generateScript_1, forwardMaxDepth? := forwardMaxDepth?_1 }) =
    (toOptions = toOptions_1 ∧ generateScript = generateScript_1 ∧ forwardMaxDepth? = forwardMaxDepth?_1)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kronecker_apply : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Mul α] (A : Matrix l m α)
  (B : Matrix n p α) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.List.toArrayAux.match_1.splitter : {α : Type u_1} →
  (motive : List α → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : Array α) →
        ((xs : Array α) → motive [] xs) →
          ((a : α) → (as : List α) → (xs : Array α) → motive (a :: as) xs) → motive x x_1
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- When `h : P ≤ Q`, this is the canonical isomorphism
`P.lift F hF ⋙ ιOfLE h ≅ Q.lift F _`.  -/
CategoryTheory.ObjectProperty.liftCompιOfLEIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        (P : CategoryTheory.ObjectProperty D) →
          {Q : CategoryTheory.ObjectProperty D} →
            (F : CategoryTheory.Functor C D) →
              (hF : ∀ (X : C), P (F.obj X)) →
                (h : P ≤ Q) → (P.lift F hF).comp (CategoryTheory.ObjectProperty.ιOfLE h) ≅ Q.lift F ⋯
-- Mathlib.Analysis.Convex.NNReal
NNReal.segment_eq_Icc : ∀ {x y : NNReal}, x ≤ y → segment NNReal x y = Set.Icc x y
-- Mathlib.Topology.Inseparable
SeparationQuotient.forall : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : SeparationQuotient X → Prop},
  (∀ (x : SeparationQuotient X), P x) ↔ ∀ (x : X), P (SeparationQuotient.mk x)
-- Mathlib.Order.RelIso.Basic
RelIso.IsWellOrder.ulift : ∀ {α : Type u} (r : α → α → Prop) [IsWellOrder α r], IsWellOrder (ULift.{u_5, u} α) (ULift.down ⁻¹'o r)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- Modifications between strong transformations of pseudofunctors are equivalent to modifications
between the underlying strong transformations of oplax functors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification.equivOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          {η θ : F ⟶ G} →
            (CategoryTheory.Pseudofunctor.StrongTrans.toOplax η).Modification
                (CategoryTheory.Pseudofunctor.StrongTrans.toOplax θ) ≃
              CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects colimits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects
limits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.reflectsLimit_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsColimit K.leftOp F],
  CategoryTheory.Limits.ReflectsLimit K F.op
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (r : ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)))
  (x : ↑X.toTopCat),
  r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.Γgerm x)) r)
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.instGeometricallyIrreducibleFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyIrreducible g],
  AlgebraicGeometry.GeometricallyIrreducible (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Tactic.Linter.Style
/-- Check `name` is a `Name` containing an underscore that should be linted against
by the `defsWithUnderscore` linter. Namely, we do not lint
* names ending in an underscore, or in a namespace ending with an underscore,
* names containing guillemets `«»` (these tend to be `term<something>` declarations,
  i.e. internal names for notation, not user-facing commands),
* names with a component starting with `term` (e.g. `Nat.term_!`)
* names starting with `Mathlib.Tactic`, `Parser` or containing a `Simps` component
  (these are probably custom simps projections, i.e. affect how `simps` names its auto-generated
  lemmas: we usually prefer a generated name `coe_support` over `coeSupport`, which requires a
  projection named `coe_support`)
* names that end in `_<number>` or in `_mathlib` (these tend to be autogenerated instance names),
* library notes.
 -/
Mathlib.Linter.Style.nameCheck.isBadNameWithUnderscore : Lean.Name → Bool
-- Mathlib.Algebra.DirectSum.Ring
_private.Mathlib.Algebra.DirectSum.Ring.0.DirectSum.mul_one : ∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] (x : DirectSum ι fun i => A i), x * 1 = x
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.assoc : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃)
  (c : ComplexShape J) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₁₂ c₃ c]
  [inst_2 : TotalComplexShape c₂ c₃ c₂₃] [inst_3 : TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mul_mem_nthRootsFinset : ∀ {R : Type u} {n : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {η₁ η₂ a₁ a₂ : R},
  η₁ ∈ Polynomial.nthRootsFinset n a₁ →
    η₂ ∈ Polynomial.nthRootsFinset n a₂ → η₁ * η₂ ∈ Polynomial.nthRootsFinset n (a₁ * a₂)
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- The basis of open subgroups for the topology on a ring determined by a valuation.  -/
Valuation.subgroups_basis : ∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
  RingSubgroupsBasis fun γ => v.ltAddSubgroup ((Units.map ↑MonoidWithZeroHom.ValueGroup₀.embedding) γ)
-- Init.Data.SInt.Lemmas
Int64.ofIntClamp_iSizeToInt : ∀ (x : ISize), Int64.ofIntClamp x.toInt = x.toInt64
-- Mathlib.Tactic.LinearCombination
Mathlib.Tactic.LinearCombination.Expanded.const.sizeOf_spec : ∀ (c : Lean.Term), sizeOf (Mathlib.Tactic.LinearCombination.Expanded.const c) = 1 + sizeOf c
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `lowerSemicontinuous_iff_isClosed_epigraph`. -/
LowerSemicontinuous.isClosed_epigraph : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [ClosedIciTopology γ] {f : α → γ}, LowerSemicontinuous f → IsClosed {p | f p.1 ≤ p.2}
-- Mathlib.MeasureTheory.PiSystem
subset_generatePiSystem_self : ∀ {α : Type u_1} (S : Set (Set α)), S ⊆ generatePiSystem S
-- Mathlib.Computability.TuringMachine.Computable
/-- proof this machine outputs `f` in at most `time(input.length)` steps  -/
Turing.TM2ComputableInTime.outputsFun : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} →
      {f : α → β} →
        (self : Turing.TM2ComputableInTime ea eb f) →
          (a : α) →
            Turing.TM2OutputsInTime self.tm (List.map self.inputAlphabet.invFun (ea a))
              (some (List.map self.outputAlphabet.invFun (eb (f a)))) (self.time (ea a).length)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_Ioc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  -Set.Ioc a b = Set.Ico (-b) (-a)
-- Init.Data.SInt.Lemmas
Int32.toInt_zero : Int32.toInt 0 = 0
-- Mathlib.Logic.Encodable.Basic
Directed.sequence_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Inhabited α] [inst_2 : Preorder β] {f : α → β}
  (hf : Directed (fun x1 x2 => x1 ≥ x2) f) (a : α), f (Directed.sequence f hf (Encodable.encode a + 1)) ≤ f a
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- If `g : FreeAbelianGroup X` and `A` is an abelian group then `liftAddGroupHom g`
is the additive group homomorphism sending a function `X → A` to the term of type `A`
corresponding to the evaluation of the induced map `FreeAbelianGroup X → A` at `g`.  -/
FreeAbelianGroup.liftAddGroupHom : {α : Type u_2} → (β : Type u_3) → [inst : AddCommGroup β] → FreeAbelianGroup α → (α → β) →+ β
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.linMulLin_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : M →ₗ[R] R} (x y : M), ((LinearMap.BilinForm.linMulLin f g) x) y = f x * g y
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [(F.comp G).PreservesEpimorphisms] [G.ReflectsEpimorphisms], F.PreservesEpimorphisms
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Any type satisfying `MulEquivClass` can be cast into `MulEquiv` via
`MulEquivClass.toMulEquiv`.  -/
instCoeTCMulEquivOfMulEquivClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : EquivLike F α β] → [inst_1 : Mul α] → [inst_2 : Mul β] → [MulEquivClass F α β] → CoeTC F (α ≃* β)
-- Mathlib.RingTheory.Morita.Matrix
/-- The image of `Eᵢᵢ` (the elementary matrix) acting on all elements in `M`.  -/
MatrixModCat.toModuleCatObj : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          (M : Type u_1) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module (Matrix ι ι R) M] →
                [inst_5 : Module R M] → [IsScalarTower R (Matrix ι ι R) M] → ι → Submodule R M
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.mul : {α : Type u_1} → [inst : MulZeroClass α] → [inst_1 : Preorder α] → [PosMulMono α] → Mul { x // 0 ≤ x }
-- Mathlib.Data.PNat.Xgcd
/-- The following function provides the starting point for
our algorithm.  We will apply an iterative reduction process
to it, which will produce a system satisfying IsReduced.
The gcd can be read off from this final system.
 -/
PNat.XgcdType.start : ℕ+ → ℕ+ → PNat.XgcdType
-- Mathlib.Data.EReal.Inv
EReal.inv_pos_of_pos_ne_top : ∀ {a : EReal}, 0 < a → a ≠ ⊤ → 0 < a⁻¹