mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A choice of the (unique) homology map data associated with a morphism
`φ : S₁ ⟶ S₂` where both short complexes `S₁` and `S₂` are equipped with
homology data.  -/
CategoryTheory.ShortComplex.HomologyMapData.homologyMapData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h₁ : S₁.HomologyData) → (h₂ : S₂.HomologyData) → CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The center vertex belongs to any ball of positive radius.  -/
SimpleGraph.mem_ball_self : ∀ {V : Type u_1} {G : SimpleGraph V} {c : V} {r : ℕ∞}, 0 < r → c ∈ G.ball c r
-- Mathlib.Topology.Sober
TopologicalSpace.IsOpenCover.quasiSober : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_3} {U : ι → TopologicalSpace.Opens α},
  TopologicalSpace.IsOpenCover U → ∀ [∀ (i : ι), QuasiSober ↥(U i)], QuasiSober α
-- Lean.Environment
Lean.Kernel.Exception.declHasFVars : Lean.Kernel.Environment → Lean.Name → Lean.Expr → Lean.Kernel.Exception
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_filter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited α] {f : α → Bool} {k : α},
  m.WF → (Std.HashSet.Raw.filter f m).get! k = (Option.filter f (m.get? k)).get!
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.single_apply : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α] (p : ENNReal)
  (i : α) (a : E i) (j : α), ↑(lp.single p i a) j = Pi.single i a j
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.isoHom.inj : ∀ {e : Lean.Expr} {isoLift : Mathlib.Tactic.BicategoryLike.IsoLift} {iso : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {e_1 : Lean.Expr} {isoLift_1 : Mathlib.Tactic.BicategoryLike.IsoLift} {iso_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso},
  Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e isoLift iso =
      Mathlib.Tactic.BicategoryLike.Mor₂.isoHom e_1 isoLift_1 iso_1 →
    e = e_1 ∧ isoLift = isoLift_1 ∧ iso = iso_1
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.add_eq_sup : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (K K' : LieSubalgebra R L), K + K' = K ⊔ K'
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rco_eq_none_iff : ∀ {m n : ℤ} {i : ℕ}, (m...n).toList[i]? = none ↔ (n - m).toNat ≤ i
-- Mathlib.Algebra.Order.Group.PosPart
instNegPart.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α], instNegPart = { negPart := fun a => -a ⊔ 0 }
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] [inst_5 : IsDedekindDomain R]
  {I J : ↥(nonZeroDivisors (Ideal R))},
  ClassGroup.mk0 I = ClassGroup.mk0 J ↔
    ∃ x, ∃ (_ : x ≠ 0), FractionalIdeal.spanSingleton (nonZeroDivisors R) x * ↑↑I = ↑↑J
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.mk.injEq : ∀ {X Y : Pointed} (toFun : X.X → Y.X) (map_point : toFun X.point = Y.point) (toFun_1 : X.X → Y.X)
  (map_point_1 : toFun_1 X.point = Y.point),
  ({ toFun := toFun, map_point := map_point } = { toFun := toFun_1, map_point := map_point_1 }) = (toFun = toFun_1)
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuous.upperHemicontinuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuous f → ∀ (x : α), UpperHemicontinuousAt f x
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.ExceptType.notComparable.sizeOf_spec : sizeOf Mathlib.Tactic.Ring.notComparable = 1
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `final_of_final_comp` below.  -/
CategoryTheory.Functor.final_of_equivalence_comp : ∀ {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.IsEquivalence] [(F.comp G).Final], G.Final
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_sub : ∀ (a b : UInt16), (a - b).toUInt32 = (a.toUInt32 - b.toUInt32) % 65536
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_eq_univ_iff : ∀ {R : Type u} [inst : CommSemiring R] (s : Set R), PrimeSpectrum.zeroLocus s = Set.univ ↔ s ⊆ ↑(nilradical R)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mem_spanSingleton_self : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x : P), x ∈ FractionalIdeal.spanSingleton S x
-- Mathlib.Order.CompleteLattice.Basic
iSup₂_eq_top : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLinearOrder α] (f : (i : ι) → κ i → α),
  ⨆ i, ⨆ j, f i j = ⊤ ↔ ∀ b < ⊤, ∃ i j, b < f i j
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.is_fg_degreeLE : ∀ {R : Type u} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal (Polynomial R)) (n : ℕ), (I.degreeLE ↑n).FG
-- Mathlib.Order.RelIso.Basic
RelIso.cast_refl : ∀ {α : Type u} {r : α → α → Prop} (h₁ : optParam (α = α) ⋯) (h₂ : optParam (r ≍ r) ⋯), RelIso.cast h₁ h₂ = RelIso.refl r
-- Mathlib.Algebra.Ring.Parity
Even.pow_of_ne_zero : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Even a → ∀ {n : ℕ}, n ≠ 0 → Even (a ^ n)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trCont.eq_def : ∀ (x : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.trCont x =
    match x with
    | Turing.ToPartrec.Cont.halt => Turing.PartrecToTM2.Cont'.halt
    | Turing.ToPartrec.Cont.cons₁ c a k => Turing.PartrecToTM2.Cont'.cons₁ c (Turing.PartrecToTM2.trCont k)
    | Turing.ToPartrec.Cont.cons₂ a k => (Turing.PartrecToTM2.trCont k).cons₂
    | Turing.ToPartrec.Cont.comp c k => Turing.PartrecToTM2.Cont'.comp c (Turing.PartrecToTM2.trCont k)
    | Turing.ToPartrec.Cont.fix c k => Turing.PartrecToTM2.Cont'.fix c (Turing.PartrecToTM2.trCont k)
-- Mathlib.Analysis.SpecificLimits.Normed
isBigO_pow_pow_of_le_left : ∀ {r₁ r₂ : ℝ}, 0 ≤ r₁ → r₁ ≤ r₂ → (fun n => r₁ ^ n) =O[Filter.atTop] fun n => r₂ ^ n
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
MonoidHom.isUniformInducing_of_isInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {Hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : Group β] [IsUniformGroup β] [inst_6 : FunLike Hom α β] [MonoidHomClass Hom α β]
  {f : Hom}, Topology.IsInducing ⇑f → IsUniformInducing ⇑f
-- Mathlib.Algebra.Group.Conj
ConjClasses.mk_injective : ∀ {α : Type u} [inst : CommMonoid α], Function.Injective ConjClasses.mk
-- Mathlib.Analysis.InnerProductSpace.Subspace
/-- An indexed family of mutually-orthogonal subspaces of an inner product space `E`.

The simple way to express this concept would be as a condition on `V : ι → Submodule 𝕜 E`.  We
instead implement it as a condition on a family of inner product spaces each equipped with an
isometric embedding into `E`, thus making it a property of morphisms rather than subobjects.
The connection to the subobject spelling is shown in `orthogonalFamily_iff_pairwise`.

This definition is less lightweight, but allows for better definitional properties when the inner
product space structure on each of the submodules is important -- for example, when considering
their Hilbert sum (`PiLp V 2`).  For example, given an orthonormal set of vectors `v : ι → E`,
we have an associated orthogonal family of one-dimensional subspaces of `E`, which it is convenient
to be able to discuss using `ι → 𝕜` rather than `Π i : ι, span 𝕜 (v i)`.  -/
OrthogonalFamily : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_4} →
            (G : ι → Type u_5) →
              [inst_3 : (i : ι) → SeminormedAddCommGroup (G i)] →
                [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] → ((i : ι) → G i →ₗᵢ[𝕜] E) → Prop
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The canonical morphism `A →ₐ[R₁] A ⧸ I` as morphism of `R₁`-algebras, for `I` an ideal of
`A`, where `A` is an `R₁`-algebra.  -/
Ideal.Quotient.mkₐ : (R₁ : Type u_1) →
  {A : Type u_3} →
    [inst : CommSemiring R₁] →
      [inst_1 : Ring A] → [inst_2 : Algebra R₁ A] → (I : Ideal A) → [inst_3 : I.IsTwoSided] → A →ₐ[R₁] A ⧸ I
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.uniqueGalXPow : {F : Type u_1} → [inst : Field F] → (n : ℕ) → Unique (Polynomial.X ^ n).Gal
-- Mathlib.Data.Set.Prod
Set.image_snd_graphOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} (f : α → β), Prod.snd '' Set.graphOn f s = f '' s
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.idealOfLE_ofPrime : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P : Ideal ↥A) [inst_1 : P.IsPrime],
  A.idealOfLE (A.ofPrime P) ⋯ = P
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereoToFun.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (v x : E),
  stereoToFun v x = (2 / (1 - ((innerSL ℝ) v) x)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto x
-- Batteries.Linter.UnreachableTactic
/-- The monad for collecting used tactic syntaxes.  -/
Batteries.Linter.UnreachableTactic.M : Type → Type
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- Notation for m×n matrices, aka `Matrix (Fin m) (Fin n) α`.

For instance:
* `!![a, b, c; d, e, f]` is the matrix with two rows and three columns, of type
  `Matrix (Fin 2) (Fin 3) α`
* `!![a, b, c]` is a row vector of type `Matrix (Fin 1) (Fin 3) α` (see also `Matrix.row`).
* `!![a; b; c]` is a column vector of type `Matrix (Fin 3) (Fin 1) α` (see also `Matrix.col`).

This notation implements some special cases:

* `![,,]`, with `n` `,`s, is a term of type `Matrix (Fin 0) (Fin n) α`
* `![;;]`, with `m` `;`s, is a term of type `Matrix (Fin m) (Fin 0) α`
* `![]` is the 0×0 matrix

Note that vector notation is provided elsewhere (by `Matrix.vecNotation`) as `![a, b, c]`.
Under the hood, `!![a, b, c; d, e, f]` is syntax for `Matrix.of ![![a, b, c], ![d, e, f]]`.
 -/
Matrix.matrixNotationRx0 : Lean.ParserDescr
-- Mathlib.GroupTheory.Index
Subgroup.index_dvd_of_le : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → K.index ∣ H.index
-- Lean.Hygiene
/-- `x._hyg...` ~> `x✝`  -/
Lean.NameSanitizerState.userName2Sanitized : Lean.NameSanitizerState → Lean.NameMap Lean.Name
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.irreducibleSpace_of_isIntegral : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X], IrreducibleSpace ↥X
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₁_eq_some_iff_utf8EncodeChar_eq : ∀ {w : UInt8} {c : Char},
  (∃ (h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done),
      ByteArray.utf8DecodeChar?.assemble₁ w h = some c) ↔
    String.utf8EncodeChar c = [w]
-- Init.Data.Option.Monadic
Option.filterM_some : ∀ {m : Type → Type u_1} {α : Type} [inst : Applicative m] (p : α → m Bool) (a : α),
  Option.filterM p (some a) = (fun b => if b = true then some a else none) <$> p a
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.findAtAux : {α : Type u_1} →
  {β : Type u_2} → [BEq α] → (keys : Array α) → (vals : Array β) → keys.size = vals.size → ℕ → α → Option β
-- Mathlib.Algebra.Order.Sub.Defs
lt_add_of_tsub_lt_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a - c < b → a < b + c
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_eq_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : LowerSet α} {t : LowerSet β},
  s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥
-- Mathlib.Tactic.Linter.UnusedTacticExtension
/-- Defines the `allowedUnusedTacticExt` extension for adding a `HashSet` of `allowedUnusedTactic`s
to the environment.
 -/
Mathlib.Linter.UnusedTactic.allowedUnusedTacticExt : Lean.SimplePersistentEnvExtension Lean.SyntaxNodeKind (Std.HashSet Lean.SyntaxNodeKind)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSumNat.brecOn.go : {motive_1 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExBaseNat e → Sort u} →
  {motive_2 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExProdNat e → Sort u} →
    {motive_3 : (e : Q(ℕ)) → Mathlib.Tactic.Ring.Common.ExSumNat e → Sort u} →
      {e : Q(ℕ)} →
        (t : Mathlib.Tactic.Ring.Common.ExSumNat e) →
          ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExBaseNat e) → t.below → motive_1 e t) →
            ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExProdNat e) → t.below → motive_2 e t) →
              ((e : Q(ℕ)) → (t : Mathlib.Tactic.Ring.Common.ExSumNat e) → t.below → motive_3 e t) →
                motive_3 e t ×' t.below
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.w_prod_snd : ∀ {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') {A B : CategoryTheory.CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (S'.map f.left.2) B.hom.2 = A.hom.2
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₈_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.b₈ = W.a₆ + 4 * W.a₂ * W.a₆
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_const : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E],
  p ≠ 0 → μ ≠ 0 → ∀ (c : E), MeasureTheory.lpNorm (fun _x => c) p μ = ‖c‖ * μ.real Set.univ ^ p.toReal⁻¹
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- Notation for `MeasurableSet` with respect to a non-standard σ-algebra.  -/
MeasureTheory.«termMeasurableSet[_]» : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that the range between two positions of `s` can be covered by longest
matches of the pattern within `s`.
 -/
String.Slice.Pattern.Model.IsLongestMatchAtChain : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → s.Pos → Prop
-- Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
/-- The map linear in the first argument and alternating in the remaining arguments that
underlies the cofactor expansion along the `M`-summand of `M × N`.  -/
_private.Mathlib.Algebra.Module.StablyFree.FreeOfInvertible.0.exteriorPower.cofactorLinear : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      {N : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] → {n : ℕ} → Module.Basis (Fin n) R N → M × N →ₗ[R] (M × N) [⋀^Fin n]→ₗ[R] M
-- Mathlib.Data.Complex.Basic
Complex.I_re : Complex.I.re = 0
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.mkCommaMorphism_right_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D} (η : F ⟶ G) (X : C),
  (CategoryTheory.WithInitial.mkCommaMorphism η).right.app X = η.app (CategoryTheory.WithInitial.incl.obj X)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerRight_left_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T) {Z : C} (h : T.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst T.hom R.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst S.hom R.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left f) h)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.subsingleton_iff_subsingleton : ∀ {R : Type u} [inst : Semiring R], Subsingleton (Polynomial R) ↔ Subsingleton R
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCommMonoid : {α : Type u_1} → [CommMonoid α] → CommMonoid αᵐᵒᵖ
-- Init.Data.List.Lemmas
List.head_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} (w : List.replicate n a ≠ []), (List.replicate n a).head w = a
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a : R), (MvPolynomial.C a).totalDegree = 0
-- Init.Data.Iterators.Combinators.Monadic.ULift
/-- Internal state of the `uLift` iterator combinator. Do not depend on its internals.  -/
Std.Iterators.Types.ULiftIterator : Type u →
  (m : Type u → Type u') →
    (n : Type (max u v) → Type v') → Type u → (⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ) → Type (max u v)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.fst_mapComp_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Prod.fst B C).mapComp f g).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.1 g.1)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.toProd_ι_tmul_one : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂) (m₁ : M₁),
  (CliffordAlgebra.toProd Q₁ Q₂) ((CliffordAlgebra.ι Q₁) m₁ ᵍ⊗ₜ[R] 1) =
    (CliffordAlgebra.ι (QuadraticMap.prod Q₁ Q₂)) (m₁, 0)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ordered_keys_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → List.Pairwise (fun a b => cmp a.1 b.1 = Ordering.lt) t.toList
-- Lean.Elab.PreDefinition.FixedParams
_private.Lean.Elab.PreDefinition.FixedParams.0.Lean.Elab.FixedParamPerm.buildArgs.go : {α : Type u_1} → Lean.Elab.FixedParamPerm → Array α → Array α → ℕ → ℕ → Array α → Array α
-- Mathlib.Logic.Equiv.Finset
_private.Mathlib.Logic.Equiv.Finset.0.Denumerable.lower'.match_1.eq_2 : ∀ (motive : List ℕ → ℕ → Sort u_1) (m : ℕ) (l : List ℕ) (n : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (m : ℕ) → (l : List ℕ) → (n : ℕ) → motive (m :: l) n),
  (match m :: l, n with
    | [], x => h_1 x
    | m :: l, n => h_2 m l n) =
    h_2 m l n
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.ExportedAxiomsState.mk.injEq : ∀ (importedModuleEntries importedModuleEntries_1 : Array (Array (Lean.Name × Array Lean.Name))),
  ({ importedModuleEntries := importedModuleEntries } = { importedModuleEntries := importedModuleEntries_1 }) =
    (importedModuleEntries = importedModuleEntries_1)
-- Std.Data.DTreeMap.Internal.Balancing
/-- Slower version of `balanceR` with weaker balancing assumptions that hold after erasing from
the left side of the tree.
 -/
Std.DTreeMap.Internal.Impl.balanceRErase : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced →
            r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size → Std.DTreeMap.Internal.Impl α β
-- Init.Data.Array.Zip
Array.zip_map : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {as : Array α} {bs : Array β},
  (Array.map f as).zip (Array.map g bs) = Array.map (Prod.map f g) (as.zip bs)
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_intCast : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (n : ℤ),
  ArchimedeanClass.stdPart ↑n = ↑n
-- Init.Data.SInt.Bitwise
Int16.ofBitVec_xor : ∀ (a b : BitVec 16), Int16.ofBitVec (a ^^^ b) = Int16.ofBitVec a ^^^ Int16.ofBitVec b
-- Std.Data.DTreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.DTreeMap.Const.ofList : {α : Type u} →
  {β : Type v} →
    List (α × β) →
      (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Const.ofList._auto_1) → Std.DTreeMap α (fun x => β) cmp
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusPolyAux_eq : ∀ (p n : ℕ),
  WittVector.frobeniusPolyAux p n =
    MvPolynomial.X (n + 1) -
      ∑ i ∈ Finset.range n,
        ∑ j ∈ Finset.range (p ^ (n - i)),
          (MvPolynomial.X i ^ p) ^ (p ^ (n - i) - (j + 1)) * WittVector.frobeniusPolyAux p i ^ (j + 1) *
            MvPolynomial.C
              ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - multiplicity p (j + 1)) * p ^ (j - multiplicity p (j + 1)))
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.shortComplexH0_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.shortComplexH0 A).g = (Rep.coinvariantsMk k G).app A
-- Mathlib.Data.List.Indexes
List.mapIdxMAux'.eq_def : ∀ {m : Type v → Type w} [inst : Monad m] {α : Type u_7} (f : ℕ → α → m PUnit.{v + 1}) (x : ℕ) (x_1 : List α),
  List.mapIdxMAux' f x x_1 =
    match x, x_1 with
    | x, [] => pure PUnit.unit
    | i, a :: as => f i a *> List.mapIdxMAux' f (i + 1) as
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyInjective : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.UniversallyInjective
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- `L` is a left adjoint  -/
CategoryTheory.ComonadicLeftAdjoint.adj : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {L : CategoryTheory.Functor C D} →
          [self : CategoryTheory.ComonadicLeftAdjoint L] → L ⊣ CategoryTheory.ComonadicLeftAdjoint.R L
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.instCanonicallyOrderedAdd : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  CanonicallyOrderedAdd (Submodule R M)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.limitsOfShape_isEmpty_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [IsEmpty J] (X : C),
  P.limitsOfShape J X ↔ Nonempty (CategoryTheory.Limits.IsTerminal X)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_comap : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N] {f : M →ₗ[R] N} {C : ConvexCone R N} {x : M},
  x ∈ ConvexCone.comap f C ↔ f x ∈ C
-- Mathlib.Algebra.Polynomial.Div
Polynomial.natDegree_divByMonic : ∀ {R : Type u} [inst : Ring R] (f : Polynomial R) {g : Polynomial R},
  g.Monic → (f /ₘ g).natDegree = f.natDegree - g.natDegree
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isCoprime_biInf : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {I : Ideal R} {J : ι → Ideal R} {s : Finset ι},
  (∀ j ∈ s, IsCoprime I (J j)) → IsCoprime I (⨅ j ∈ s, J j)