mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.mkH1OfIsTrivial.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  groupHomology.mkH1OfIsTrivial A = groupHomology.mkH1OfIsTrivial A
-- Lean.Elab.Command
Lean.Elab.Command.instToSnapshotTreeMacroExpandedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.Command.MacroExpandedSnapshot
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.instSymmetricCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.SymmetricCategory C] →
          [inst_3 : P.IsStableUnderBraiding] → CategoryTheory.SymmetricCategory (CategoryTheory.WideSubcategory P)
-- Mathlib.Computability.RegularExpressions
RegularExpression.deriv_zero : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), RegularExpression.deriv 0 a = 0
-- Init.Data.UInt.Bitwise
UInt64.ofBitVec_shiftLeft : ∀ (a : BitVec 64), ∀ b < 64, { toBitVec := a <<< b } = { toBitVec := a } <<< UInt64.ofNat b
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.hasCompactSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  (f : CompactlySupportedContinuousMap α β), HasCompactSupport ⇑f
-- Mathlib.LinearAlgebra.Ray
/-- If two vectors are on the same ray then both scaled by the same action are also on the same
ray.  -/
SameRay.smul : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {x y : M} {S : Type u_6} [inst_5 : Monoid S]
  [inst_6 : DistribMulAction S M] [SMulCommClass R S M], SameRay R x y → ∀ (s : S), SameRay R (s • x) (s • y)
-- Mathlib.Topology.Compactness.Lindelof
countable_of_Lindelof_of_discrete : ∀ {X : Type u} [inst : TopologicalSpace X] [LindelofSpace X] [DiscreteTopology X], Countable X
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Expr.updateLetS! : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Topology.Order.Compact
cocompact_le_atBot_atTop : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α],
  Filter.cocompact α ≤ Filter.atBot ⊔ Filter.atTop
-- Init.Data.Array.Find
Array.findIdx_le_size : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.findIdx p xs ≤ xs.size
-- Mathlib.RepresentationTheory.Basic
Representation.finsupp_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : AddCommMonoid A]
  [inst_3 : Module k A] (ρ : Representation k G A) (α : Type u_6) (g : G),
  (ρ.finsupp α) g = (Finsupp.lsum k) fun i => Finsupp.lsingle i ∘ₗ ρ g
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_lt : ∀ {a b : UInt64}, a.toUInt32 < b.toUInt32 ↔ a % 4294967296 < b % 4294967296
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instSMulSubtypeMem : {M' : Type u_1} → {α : Type u_2} → {S' : Type u_4} → [inst : SetLike S' M'] → (s : S') → [SMul M' α] → SMul (↥s) α
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.mem_gradeBy_iff : ∀ {M : Type u_1} {ι : Type u_2} (R : Type u_3) [inst : CommSemiring R] (f : M → ι) (i : ι) (a : AddMonoidAlgebra R M),
  a ∈ AddMonoidAlgebra.gradeBy R f i ↔ ↑a.coeff.support ⊆ f ⁻¹' {i}
-- Batteries.Data.RunningStats
/-- Standard deviation of running data stream (square-root of population variance).  -/
Batteries.RunningStats.standardDeviation : Batteries.RunningStats → Float
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.isCompl_mk_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule),
  IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl p q
-- Init.Data.List.Nat.Modify
List.modifyHead_eq_modify_zero : ∀ {α : Type u_1} (f : α → α) (l : List α), List.modifyHead f l = l.modify 0 f
-- Mathlib.CategoryTheory.Localization.Construction
/-- The lifting of a functor to the path category of `LocQuiver W`  -/
CategoryTheory.Localization.Construction.liftToPathCategory : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {D : Type uD} →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] →
          (G : CategoryTheory.Functor C D) →
            W.IsInvertedBy G →
              CategoryTheory.Functor (CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)) D
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiff.dist : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f g : G → E}
  {n : WithTop ℕ∞}, ContDiff ℝ n f → ContDiff ℝ n g → (∀ (x : G), f x ≠ g x) → ContDiff ℝ n fun y => dist (f y) (g y)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le : ∀ {α : Type u_1} {β : Type u_5} {f : α → β} [inst : NormedAddCommGroup β] [inst_1 : NormedSpace ℝ β]
  {m : MeasurableSpace α} (hf : MeasureTheory.StronglyMeasurable f) {c : ℝ} {x : α},
  ‖f x‖ ≤ c → Filter.Tendsto (fun n => (hf.approxBounded c n) x) Filter.atTop (nhds (f x))
-- Mathlib.Control.Bitraversable.Instances
Bitraversable.traversable : {t : Type u → Type u → Type u} → [Bitraversable t] → {α : Type u} → Traversable (t α)
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instHasHomologyOppositeOp : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex V c) (i : ι) [K.HasHomology i],
  K.op.HasHomology i
-- Lean.Parser.Command
/-- `open Foo in e` is like `open Foo` but scoped to a single term.
It makes the given namespaces available in the term `e`.
 -/
Lean.Parser.Term.open : Lean.Parser.Parser
-- Mathlib.Data.QPF.Univariate.Basic
/-- does recursion on `q.P.W` using `g : F α → α` rather than `g : P α → α`  -/
QPF.recF : {F : Type u → Type v} → [q : QPF F] → {α : Type u} → (F α → α) → (QPF.P F).W → α
-- Mathlib.Topology.Order
mem_nhds_discrete : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α] {x : α} {s : Set α}, s ∈ nhds x ↔ x ∈ s
-- Init.Data.Vector.Range
Vector.zipIdx_map_fst : ∀ {α : Type u_1} {n : ℕ} (i : ℕ) (xs : Vector α n), Vector.map Prod.fst (xs.zipIdx i) = xs
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.algebraMap_toAddMonoid_hom : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι] [inst_4 : DirectSum.GSemiring A]
  [inst_5 : DirectSum.GAlgebra R A] [inst_6 : DecidableEq ι],
  ↑(algebraMap R (DirectSum ι fun i => A i)) = (DirectSum.of A 0).comp DirectSum.GAlgebra.toFun
-- Mathlib.Order.RelSeries
/-- In ℤ, two entries in an `LTSeries` differ by at least the difference of their indices.
(Expressed in a way that avoids subtraction).
 -/
LTSeries.apply_add_index_le_apply_add_index_int : ∀ (p : LTSeries ℤ) (i j : Fin (p.length + 1)), i ≤ j → p.toFun i + ↑↑j ≤ p.toFun j + ↑↑i
-- Batteries.Data.List.Basic
List.takeListTR.go.eq_1 : ∀ {α : Type u_1} (a : List α) (a_1 : Array (List α)), List.takeListTR.go [] a a_1 = (a_1.toList, a)
-- Init.Data.SInt.Bitwise
Bool.toInt32.eq_1 : ∀ (b : Bool), b.toInt32 = if b = true then 1 else 0
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The forward function of a measurable equivalence is measurable.  -/
MeasurableEquiv.measurable_toFun : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (self : α ≃ᵐ β),
  Measurable ⇑self.toEquiv
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.toList_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.toList = t₂.toList
-- Mathlib.Algebra.Group.Hom.Defs
/-- The hom class hierarchy allows for a single lemma, such as `map_one`, to apply to a large variety
of morphism types, so long as they have an instance of `OneHomClass`. For example, this applies to
to `MonoidHom`, `RingHom`, `AlgHom`, `StarAlgHom`, as well as their `Equiv` variants, etc. However,
precisely because these lemmas are so widely applicable, they keys in the `simp` discrimination tree
are necessarily highly non-specific. For example, the key for `map_one` is
`@DFunLike.coe _ _ _ _ _ 1`.

Consequently, whenever lean sees `⇑f 1`, for some `f : F`, it will attempt to synthesize a
`OneHomClass F ?A ?B` instance. If no such instance exists, then Lean will need to traverse (almost)
the entirety of the `FunLike` hierarchy in order to determine this because so many classes have a
`OneHomClass` instance (in fact, this problem is likely worse for `ZeroHomClass`). This can lead to
a significant performance hit when `map_one` fails to apply.

To avoid this problem, we mark these widely applicable simp lemmas with key discrimination tree keys
with `mid` priority in order to ensure that they are not tried first.

We do not use `low`, to allow bundled morphisms to unfold themselves with `low` priority such that
the generic morphism lemmas are applied first. For instance, we might have
```lean
def fooMonoidHom : M →* N where
  toFun := foo; map_one' := sorry; map_mul' := sorry

@[simp low] lemma fooMonoidHom_apply (x : M) : fooMonoidHom x = foo x := rfl
```
As `map_mul` is tagged `simp mid`, this means that it still fires before `fooMonoidHom_apply`, which
is the behavior we desire.
 -/
LibraryNote.hom_simp_lemma_priority : Batteries.Util.LibraryNote
-- Init.Data.Vector.Find
Vector.mem_of_find?_eq_some : ∀ {α : Type} {n : ℕ} {p : α → Bool} {a : α} {xs : Vector α n}, Vector.find? p xs = some a → a ∈ xs
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.instInv : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → Inv (SpecialLinearGroup R V)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.coe_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (f : r ↪r s)
  (g : s ↪r t), ⇑(f.trans g) = ⇑g ∘ ⇑f
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0`, `+`, unary `-`, and binary `-` is a
`SubNegZeroMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and binary
`-` to a `SubNegZeroMonoid`. This version takes custom `nsmul` and `zsmul` as `[SMul ℕ M₁]` and
`[SMul ℤ M₁]` arguments.  -/
Function.Injective.subNegZeroMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : Neg M₁] →
            [inst_4 : Sub M₁] →
              [inst_5 : SMul ℤ M₁] →
                [inst_6 : SubNegZeroMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 0 = 0 →
                        (∀ (x y : M₁), f (x + y) = f x + f y) →
                          (∀ (x : M₁), f (-x) = -f x) →
                            (∀ (x y : M₁), f (x - y) = f x - f y) →
                              (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → SubNegZeroMonoid M₁
-- Lean.Declaration
/-- Number of minor premises  -/
Lean.RecursorVal.numMinors : Lean.RecursorVal → ℕ
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovEDist_ne_top : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν], MeasureTheory.levyProkhorovEDist μ ν ≠ ⊤
-- Mathlib.Algebra.Order.Chebyshev
/-- Special case of **Jensen's inequality** for sums of powers.  -/
pow_sum_le_card_mul_sum_pow : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {f : ι → α},
  (∀ i ∈ s, 0 ≤ f i) → ∀ (n : ℕ), (∑ i ∈ s, f i) ^ (n + 1) ≤ ↑s.card ^ n * ∑ i ∈ s, f i ^ (n + 1)
-- Mathlib.Tactic.GRewrite.Elab
/-- `apply_rw [e₁, ..., eₙ]` uses the expressions `e₁`, ..., `eₙ` as generalized rewrite rules, of type
`pᵢ → qᵢ`, on the main goal, replacing occurrences of `pᵢ` with `qᵢ`. The difference with `grw` is
that `grw` would turn `pᵢ` into a side goal and expect `qᵢ` to be a relation.

If an expression `e` is a defined constant, then the equational theorems associated with `e` are
used. This provides a convenient way to unfold `e`.

* `apply_rw [← e]` applies the rewrite rule `e : p → q` in the reverse direction, replacing
  occurrences of `q` with `p`.
* `apply_rw (config := cfg) [e₁, ..., eₙ]` uses `cfg` as configuration. See `GRewrite.Config`
  for details.
  To let `apply_rw` unfold more aggressively, as in `erw`, use
  `apply_rw (transparency := default) [e₁, ..., eₙ]`.
* `apply_rw [e₁, ..., eₙ] at l` rewrites at the location(s) `l`.
 -/
Mathlib.Tactic.GRewrite.applyRwSeq : Lean.ParserDescr
-- Init.Data.List.Find
List.Sublist.lookup_isSome : ∀ {α : Type u_2} [inst : BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)},
  l₁.Sublist l₂ → (List.lookup k l₁).isSome = true → (List.lookup k l₂).isSome = true
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x`, `1 x = 1`, and `(f ^ n) x = f x ^ n`
is a right cancel monoid if `β` is a right cancel monoid.  -/
FunLike.rightCancelMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : RightCancelMonoid β] →
                [IsOneApply F α β] → [IsMulApply F α β] → [IsPowApply ℕ F α β] → RightCancelMonoid F
-- Std.Data.HashSet.Basic
/-- Checks whether an element is present in a set and inserts the element if it was not found.
If the hash set already contains an element that is equal (with regard to `==`) to the given
element, then the hash set is returned unchanged.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.HashSet.containsThenInsert : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → α → Bool × Std.HashSet α
-- Std.Data.DTreeMap.Internal.Operations
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.beq : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.LawfulEqOrd α] →
        [(k : α) → BEq (β k)] → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Bool
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- Construct a `Subsemiring R` from a set `s`, a submonoid `sm`, and an additive
submonoid `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`.  -/
Subsemiring.mk' : {R : Type u} →
  [inst : NonAssocSemiring R] →
    (s : Set R) → (sm : Submonoid R) → ↑sm = s → (sa : AddSubmonoid R) → ↑sa = s → Subsemiring R
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.coe_id : ∀ {X : AddCommMonCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Std.Sat.AIG.CachedGates
/-- Create an and gate in the input AIG. This uses the builtin cache to enable automated subterm
sharing.
 -/
Std.Sat.AIG.mkAndCached : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
-- Init.Data.UInt.Bitwise
UInt16.toUInt8_not : ∀ (a : UInt16), (~~~a).toUInt8 = ~~~a.toUInt8
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.isLocalExtr_T_real_iff : ∀ {n : ℕ},
  2 ≤ n →
    ∀ (x : ℝ),
      IsLocalExtr (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n)) x ↔
        ∃ k ∈ Finset.Ioo 0 n, x = Real.cos (↑k * Real.pi / ↑n)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- `A.det` is invertible if `A` has a right inverse.  -/
Matrix.detInvertibleOfRightInverse : {n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A B : Matrix n n α) → A * B = 1 → Invertible A.det
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.restriction_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) {X Y : Cᵒᵖ}
  (f : X ⟶ Y) (M : PresheafOfModules R), (PresheafOfModules.restriction R f).app M = M.map f
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.starGraph_center_adj : ∀ {V : Type u_1} {r v : V}, r ≠ v → (SimpleGraph.starGraph r).Adj r v
-- Std.Time.Format.Basic
/-- Constructs a new `GenericFormat` specification for a date-time string. Modifiers can be combined to create
custom formats, such as "YYYY, MMMM, D".
 -/
Std.Time.GenericFormat.spec : {tz : Std.Time.Awareness} → String → optParam Std.Time.FormatConfig { } → Except String (Std.Time.GenericFormat tz)
-- Mathlib.Analysis.Calculus.TangentCone.Basic
uniqueDiffWithinAt_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E],
  UniqueDiffWithinAt 𝕜 (closure s) x ↔ UniqueDiffWithinAt 𝕜 s x
-- Lean.DocString.Markdown
/-- Registers a builtin block Markdown renderer.  -/
Lean.Doc.addBuiltinBlockMdRenderer : Lean.Name → Lean.Doc.BlockMdRenderer → IO Unit
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- `baseChange A f` for `f : M →ₗ[R] N` is the `A`-linear map `A ⊗[R] M →ₗ[A] A ⊗[R] N`.

This "base change" operation is also known as "extension of scalars".  -/
LinearMap.baseChange : {R : Type u_1} →
  (A : Type u_2) →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → (M →ₗ[R] N) → TensorProduct R A M →ₗ[A] TensorProduct R A N
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyClass.mk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  Function.Surjective HomotopicalAlgebra.RightHomotopyClass.mk
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_uIoo_castAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m ⁻¹' Set.uIoo (Fin.castAdd m i) (Fin.castAdd m j) = Set.uIoo i j
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.keys_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {f : α → β → γ},
  m.WF → (Std.HashMap.Raw.map f m).keys.Perm m.keys
-- Mathlib.Order.Bounds.Basic
isLUB_Ico : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] [DenselyOrdered γ] {a b : γ}, b < a → IsLUB (Set.Ico b a) a
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.op_codiagonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f],
  (CategoryTheory.Limits.pushout.codiagonal f).op =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f.op)
      (CategoryTheory.Limits.pullbackIsoOpPushout f.op f.op).hom
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_adjunction_id_symm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c : B} {l r : c ⟶ c}
  (adj : CategoryTheory.Bicategory.Adjunction l r) (α : r ⟶ CategoryTheory.CategoryStruct.id c),
  (CategoryTheory.Bicategory.conjugateEquiv adj (CategoryTheory.Bicategory.Adjunction.id c)).symm α =
    CategoryTheory.CategoryStruct.comp adj.unit
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft l α)
        (CategoryTheory.Bicategory.rightUnitor l).hom)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C)
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B))
      (F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst A B)) =
    CategoryTheory.SemiCartesianMonoidalCategory.fst (F.obj A) (F.obj B)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The approximation sequence converges at the successor of the domain's cardinality
to the least fixed point if starting from `⊥`  -/
OrdinalApprox.lfpApprox_ord_eq_lfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α),
  OrdinalApprox.lfpApprox f ⊥ (Order.succ (Cardinal.mk α)).ord = OrderHom.lfp f
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftAux_self_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ)
  [inst_2 : IsPRadical i p] [inst_3 : ExpChar L p] [inst_4 : PerfectRing L p] (x : L), PerfectRing.liftAux i i p x = x
-- Mathlib.Data.BitVec
BitVec.instCommRing : {w : ℕ} → CommRing (BitVec w)
-- Init.Data.Int.Basic
/-- The canonical homomorphism `Int → R`. In most use cases, the target type will have a ring structure,
and this homomorphism should be a ring homomorphism.

`IntCast` and `NatCast` exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent `simp` normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
`IntCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus an
`IntCast R` instance) whenever `R` is an additive group with a `1`.
 -/
IntCast : Type u → Type u
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.toLinearOrderMultispanIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [inst_1 : LinearOrder ι]
  (X : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)),
  I.toLinearOrderMultispanIso.hom.app X =
    (match X with
      | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Iso.refl (I.left ↑a)
      | CategoryTheory.Limits.WalkingMultispan.right a => CategoryTheory.Iso.refl (I.right a)).hom
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.nonneg : ∀ {ι : Type uι} {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] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) (i : ι) (x : M), 0 ≤ (f i) x
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.exists_setOfPred_restrict_le_iff`. -/
Valuation.exists_setOf_restrict_le_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] (x : R) (s : Set R),
  (∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (ValuativeRel.valuation R) (a - x) < ↑γ} ⊆ s
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.cidx : Lean.IR.CtorInfo → ℕ