mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote_toPoly'_go : ∀ {k : ℤ} {p : Int.Internal.Linear.Poly} (ctx : Int.Internal.Linear.Context) (e : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Expr.toPoly'.go k e p) =
    k * Int.Internal.Linear.Expr.denote ctx e + Int.Internal.Linear.Poly.denote ctx p
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.toDistribMulActionHom : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        {φ : R →* S} →
          {A : Type v} →
            {B : Type w} →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] → [inst_5 : DistribMulAction S B] → (A →ₛₙₐ[φ] B) → A →ₑ+[φ] B
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.c₄ = W.b₂ ^ 2
-- Init.SimpLemmas
ne_eq : ∀ {α : Sort u_1} (a b : α), (a ≠ b) = ¬a = b
-- Mathlib.CategoryTheory.Shift.CommShift
/-- If `e : F ≅ G` is an isomorphism of functors and if `F` commutes with the
shift, then `G` also commutes with the shift.  -/
CategoryTheory.Functor.CommShift.ofIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F G : CategoryTheory.Functor C D} →
          (F ≅ G) →
            (A : Type u_4) →
              [inst_2 : AddMonoid A] →
                [inst_3 : CategoryTheory.HasShift C A] →
                  [inst_4 : CategoryTheory.HasShift D A] → [F.CommShift A] → G.CommShift A
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.degree_pos_of_not_isUnit_of_dvd_monic : ∀ {R : Type u} [inst : CommSemiring R] {a p : Polynomial R}, p.Monic → ¬IsUnit a → a ∣ p → 0 < a.degree
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.BVVar.mk.sizeOf_spec : ∀ {width : ℕ} (ident : ℕ), sizeOf { ident := ident } = 1 + sizeOf ident
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.asymptoticNhds_smul : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V) {c : k},
  0 < c → AffineSpace.asymptoticNhds k P (c • v) = AffineSpace.asymptoticNhds k P v
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.inductionOn : ∀ {α₁ : Type u_2} {rels₁ : FreeAddMonoid α₁ → FreeAddMonoid α₁ → Prop} {δ : PresentedAddMonoid rels₁ → Prop}
  (q : PresentedAddMonoid rels₁), (∀ (a : FreeAddMonoid α₁), δ ((PresentedAddMonoid.mk rels₁) a)) → δ q
-- Mathlib.Data.Int.Cast.Basic
Int.cast_ite : ∀ {R : Type u} [inst : IntCast R] (P : Prop) [inst_1 : Decidable P] (m n : ℤ),
  ↑(if P then m else n) = if P then ↑m else ↑n
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instIsStrictOrderedRingCastInt : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d], IsStrictOrderedRing (ℤ√↑d)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.instPreservesFiniteProducts : ∀ {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) [F.Monoidal], CategoryTheory.Limits.PreservesFiniteProducts F
-- Init.Data.SInt.Basic
/-- The power operation, raising a 32-bit signed integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
Int32.pow : Int32 → ℕ → Int32
-- Mathlib.Analysis.Convex.Gauge
gaugeSeminorm_lt_one_of_isOpen : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : RCLike 𝕜]
  [inst_3 : Module 𝕜 E] [inst_4 : IsScalarTower ℝ 𝕜 E] {hs₀ : Balanced 𝕜 s} {hs₁ : Convex ℝ s} {hs₂ : Absorbent ℝ s}
  [inst_5 : TopologicalSpace E] [ContinuousSMul ℝ E], IsOpen s → ∀ {x : E}, x ∈ s → (gaugeSeminorm hs₀ hs₁ hs₂) x < 1
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.unitsLift.eq_1 : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : Monoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousMul M],
  ContinuousMap.unitsLift =
    {
      toFun := fun f =>
        { val := { toFun := fun x => ↑(f x), continuous_toFun := ⋯ },
          inv := { toFun := fun x => ↑(f x)⁻¹, continuous_toFun := ⋯ }, val_inv := ⋯, inv_val := ⋯ },
      invFun := fun f =>
        { toFun := fun x => { val := ↑f x, inv := ↑f⁻¹ x, val_inv := ⋯, inv_val := ⋯ }, continuous_toFun := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.comm₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp self.m₁ v₁₃ = v₁₂
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `ite p a b`,
such that `positivity` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.Positivity.evalIte : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.equivOfEquiv_algebraMap : ∀ {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field L]
  [inst_3 : Field M] [inst_4 : Algebra R M] [inst_5 : Module.IsTorsionFree R M] [inst_6 : IsAlgClosure R M]
  [inst_7 : Algebra S L] [inst_8 : Module.IsTorsionFree S L] [inst_9 : IsAlgClosure S L] [inst_10 : IsDomain R]
  [inst_11 : IsDomain S] (hSR : S ≃+* R) (s : S),
  (IsAlgClosure.equivOfEquiv L M hSR) ((algebraMap S L) s) = (algebraMap R M) (hSR s)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.ext_iff : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  {h h' : IsAdjoinRoot S f}, h = h' ↔ h.root = h'.root
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_forall_constGet?_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [LawfulBEq α],
  m₁.WF → m₂.WF → (∀ (k : α), Std.DHashMap.Raw.Const.get? m₁ k = Std.DHashMap.Raw.Const.get? m₂ k) → m₁.Equiv m₂
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.add_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x y : R}, x ∈ I → y ∈ I → x + y ∈ I
-- Lean.Meta.Basic
Lean.Meta.whnfForall : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.UInt.Lemmas
Nat.toUInt32_eq : ∀ {n : ℕ}, n.toUInt32 = UInt32.ofNat n
-- Init.Data.List.Zip
List.zipWith_append : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l₁ l₁' : List α} {l₂ l₂' : List β},
  l₁.length = l₂.length → List.zipWith f (l₁ ++ l₁') (l₂ ++ l₂') = List.zipWith f l₁ l₂ ++ List.zipWith f l₁' l₂'
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.abs_ediv_le_abs : ∀ (a b : ℤ), |a / b| ≤ |a|
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat.sizeOf_spec : ∀ (a b : Lean.Expr) (natStructId : ℕ) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat a b natStructId lhs rhs) =
    1 + sizeOf a + sizeOf b + sizeOf natStructId + sizeOf lhs + sizeOf rhs
-- Batteries.Util.ProofWanted
/-- The wanted declaration this dependency stands for; used to deduplicate against other
references made by the enclosing declaration.  -/
_private.Batteries.Util.ProofWanted.0.WantedDep.name : WantedDep✝ → Lean.Name
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The centralizer of the star-closure of a set as a non-unital star subalgebra.  -/
NonUnitalStarSubalgebra.centralizer : (R : Type u) →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : StarRing A] →
          [inst_3 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Set A → NonUnitalStarSubalgebra R A
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneous_span : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (s : Set A), (∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x) → Ideal.IsHomogeneous 𝒜 (Ideal.span s)
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by all the matrices in `listTransvecCol M` does not change the last row.  -/
Matrix.Pivot.listTransvecCol_mul_last_row : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit),
  ((Matrix.Pivot.listTransvecCol M).prod * M) (Sum.inr ()) i = M (Sum.inr ()) i
-- Mathlib.FieldTheory.LinearDisjoint
/-- Linear disjointness is preserved by algebra homomorphism.  -/
IntermediateField.LinearDisjoint.map'' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E] {L' : Type u_1} [inst_7 : Field L']
  [inst_8 : Algebra F L'] [inst_9 : Algebra L' E] [inst_10 : IsScalarTower F L' E],
  (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L' →
    ∀ (K : Type u_2) [inst_11 : Field K] [inst_12 : Algebra F K] [inst_13 : Algebra L K] [inst_14 : IsScalarTower F L K]
      [inst_15 : Algebra L' K] [inst_16 : IsScalarTower F L' K] [inst_17 : Algebra E K] [IsScalarTower F E K]
      [IsScalarTower L E K] [IsScalarTower L' E K], (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint L'
-- Mathlib.Order.Filter.IsBounded
Filter.bddBelow_range_of_tendsto_atBot_atTop : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [IsCodirectedOrder α] {u : ℕ → α},
  Filter.Tendsto u Filter.atTop Filter.atTop → BddBelow (Set.range u)
-- Mathlib.GroupTheory.CoprodI
/-- The equivalence between words and pairs. Given a word, it decomposes it as a pair by removing
the first letter if it comes from `M i`. Given a pair, it prepends the head to the tail.  -/
Monoid.CoprodI.Word.equivPair : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      [DecidableEq ι] → [(i : ι) → DecidableEq (M i)] → (i : ι) → Monoid.CoprodI.Word M ≃ Monoid.CoprodI.Word.Pair M i
-- Mathlib.SetTheory.Ordinal.Notation
NONote.repr_add : ∀ (a b : NONote), (a + b).repr = a.repr + b.repr
-- Mathlib.Algebra.Group.Pointwise.Finset.Density
Finset.dens_inv : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] [inst_2 : Fintype α] (s : Finset α),
  s⁻¹.dens = s.dens
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSliceData.mk.injEq : ∀ {α : Type u} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Rio α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Rio α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- `n ↦ ∐ₙ X` is left adjoint to `Hom(X, -)`.  -/
CategoryTheory.Limits.sigmaConstAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      (X : C) → CategoryTheory.Limits.sigmaConst.obj X ⊣ CategoryTheory.coyoneda.obj (Opposite.op X)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Equiv.prod_comp : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : CommMonoid M]
  (e : ι ≃ κ) (g : κ → M), ∏ i, g (e i) = ∏ i, g i
-- Mathlib.Topology.Subpath
/-- **Alias** of `Set.Icc.continuous_convexComb_prod`. -/
Path.subpathAux_continuous : ∀ {a b : ℝ}, Continuous fun x => Set.Icc.convexComb x.1 x.2.1 x.2.2
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.monomial_mul_modMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (s : σ →₀ ℕ) (x : MvPolynomial σ R),
  ((MvPolynomial.monomial s) 1 * x).modMonomial s = 0
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.leftOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {L : CategoryTheory.Functor C Dᵒᵖ},
  W.IsInvertedBy L → W.op.IsInvertedBy L.leftOp
-- Batteries.Lean.LawfulMonad
instLawfulMonadEIO_batteries : ∀ {ε : Type}, LawfulMonad (EIO ε)
-- Mathlib.Logic.Function.Coequalizer
/-- Any map `u : β → γ` with `u ∘ f = u ∘ g` factors via `Function.Coequalizer.mk`.  -/
Function.Coequalizer.desc : {α : Type u_1} →
  {β : Type u_2} → (f g : α → β) → {γ : Type u_3} → (u : β → γ) → u ∘ f = u ∘ g → Function.Coequalizer f g → γ
-- Mathlib.CategoryTheory.Category.TwoP
/-- The functor from `Pointed` to `TwoP` which adds a second point.  -/
pointedToTwoPFst : CategoryTheory.Functor Pointed TwoP
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- `α →₁[μ] E` is the type of `L¹` or integrable functions from `α` to `E`.  -/
MeasureTheory.«term_→₁[_]_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.Linter.PrivateModule
/-- The `privateModule` linter lints against nonempty modules that have only private declarations,
and suggests adding `@[expose] public section` to the top.

This linter only acts on the end-of-input `Parser.Command.eoi` token, and ignores all other syntax.
It logs its message at the top of the file.
 -/
_private.Mathlib.Tactic.Linter.PrivateModule.0.Mathlib.Linter.privateModule : Lean.Linter
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : Add Mᵃᵒᵖ], DomAddAct.instAddOfAddOpposite = inst
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Lex.acc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop},
  (∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0) →
    (∀ (i : ι), WellFounded (s i)) →
      ∀ [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)] (x : Π₀ (i : ι), α i),
        (∀ i ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) i) → Acc (DFinsupp.Lex r s) x
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- Let `A', A, B', B` be subgroups of `G`. If `A' = B'` and `A = B`, then the
quotients `A / (A' ⊓ A)` and `B / (B' ⊓ B)` are isomorphic. Applying this equiv is nicer than
rewriting along the equalities, since the type of `(A'.addSubgroupOf A : AddSubgroup A)` depends on
`A`.  -/
QuotientAddGroup.equivQuotientAddSubgroupOfOfEq : {G : Type u} →
  [inst : AddGroup G] →
    {A' A B' B : AddSubgroup G} →
      [hAN : (A'.addSubgroupOf A).Normal] →
        [hBN : (B'.addSubgroupOf B).Normal] → A' = B' → A = B → ↥A ⧸ A'.addSubgroupOf A ≃+ ↥B ⧸ B'.addSubgroupOf B
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedEqCnstrProof : Inhabited Lean.Meta.Grind.Arith.CommRing.EqCnstrProof
-- Mathlib.CategoryTheory.Subobject.Comma
/-- If `A : S → T.obj B` is a structured arrow for `S : D` and `T : C ⥤ D`, then we can explicitly
describe the subobjects of `A` as the subobjects `P` of `B` in `C` for which `A.hom` factors
through the image of `P` under `T`.  -/
CategoryTheory.StructuredArrow.subobjectEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            [CategoryTheory.Limits.HasFiniteLimits C] →
              [CategoryTheory.Limits.PreservesFiniteLimits T] →
                (A : CategoryTheory.StructuredArrow S T) →
                  CategoryTheory.Subobject A ≃o
                    { P // ∃ q, CategoryTheory.CategoryStruct.comp q (T.map P.arrow) = A.hom }
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.linearEquiv.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [inst_7 : IsLocalizedModule S f]
  [inst_8 : IsLocalizedModule S g],
  IsLocalizedModule.linearEquiv S f g = (IsLocalizedModule.iso S f).symm.trans (IsLocalizedModule.iso S g)
-- Mathlib.Topology.Instances.Int
Int.instProperSpace : ProperSpace ℤ
-- Lean.Parser.Term
Lean.Parser.Term.local : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.image_finsetProd_pi`.

---

The n-ary version of `Set.image_mul_prod`.  -/
Set.image_finset_prod_pi : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] (l : Finset ι) (S : ι → Set α),
  (fun f => ∏ i ∈ l, f i) '' (↑l).pi S = ∏ i ∈ l, S i
-- Mathlib.Probability.Kernel.Defs
/-- A sequence of finite kernels such that `κ = ProbabilityTheory.Kernel.sum (seq κ)`. See
`ProbabilityTheory.Kernel.isFiniteKernel_seq` and `ProbabilityTheory.Kernel.kernel_sum_seq`.  -/
ProbabilityTheory.Kernel.seq : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (κ : ProbabilityTheory.Kernel α β) →
          [h : ProbabilityTheory.IsSFiniteKernel κ] → ℕ → ProbabilityTheory.Kernel α β
-- Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.Grind.withConfigItems : {α : Type} → Array Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM α → Lean.Elab.Tactic.Grind.GrindTacticM α
-- Mathlib.Algebra.Field.Defs
Field.toNNRatCast : {K : Type u} → [self : Field K] → NNRatCast K
-- Mathlib.RingTheory.Smooth.Fiber
_private.Mathlib.RingTheory.Smooth.Fiber.0.Algebra.«term𝓂[_]» : Lean.ParserDescr
-- Lean.Util.MonadBacktrack
Lean.MonadBacktrack.mk : {s : outParam Type} → {m : Type → Type} → m s → (s → m Unit) → Lean.MonadBacktrack s m
-- Mathlib.Util.Notation3
/-- The initial state.  -/
Mathlib.Notation3.MatchState.empty : Mathlib.Notation3.MatchState
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Traverses the given expression `e`, and invokes the continuation `k`
at every saturated call to `recFnName`.

The expression `param` is passed along, and refined when going under a matcher
or `casesOn` application.
 -/
Lean.Elab.WF.GuessLex.withRecApps : {α : Type} → Lean.Name → ℕ → Lean.Expr → Lean.Expr → (Lean.Expr → Array Lean.Expr → Lean.MetaM α) → Lean.MetaM (Array α)
-- Std.Http.Data.Body.Stream
/-- A single blocked producer waiting for a receiver.
 -/
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.State.pendingProducer : Std.Http.Body.Channel.State✝ → Option Std.Http.Body.Channel.Producer✝
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
/-- `Nat.doubleFactorial n` is the double factorial of `n`.  -/
Nat.«term_‼» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.bound : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F),
  ∃ C, 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
-- Mathlib.Data.List.Cycle
Cycle.coe_nil : ∀ {α : Type u_1}, ↑[] = Cycle.nil
-- Init.Data.SInt.Basic
/-- Adds two 8-bit signed integers, wrapping around on over- or underflow. Usually accessed via the `+`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.add : Int8 → Int8 → Int8
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_prod : ∀ {K : Type u_1} [inst : RCLike K] {α : Type u_3} (s : Finset α) (f : α → ℝ), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.liftOfStrictSegal.f₂.eq_1 : ∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ }))
  (f₁ :
    X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ }))
  (hδ₁ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hδ₀ :
    ∀ (x : X.obj (Opposite.op { obj := { len := 1 }, property := _proof_12✝ })),
      f₀ ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) x) =
        (CategoryTheory.ConcreteCategory.hom (Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝ _proof_13✝).op)) (f₁ x))
  (hY : Y.StrictSegal) (x : X.obj (Opposite.op { obj := { len := 2 }, property := _proof_14✝ })),
  SSet.Truncated.liftOfStrictSegal.f₂ f₀ f₁ hδ₁ hδ₀ hY x =
    (hY.spineEquiv 2 SSet.Truncated.liftOfStrictSegal.f₂._proof_5).symm
      ((Y.spine 1 SSet.Truncated.liftOfStrictSegal.f₂._proof_6
            (f₁
              ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝ _proof_15✝).op))
                x))).mk₂
        (Y.spine 1 SSet.Truncated.liftOfStrictSegal.f₂._proof_6
          (f₁
            ((CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝ _proof_15✝).op))
              x)))
        ⋯)
-- Lean.Meta.Match.Match
Lean.Meta.Match.isCurrVarInductive : Lean.Meta.Match.Problem → Lean.MetaM Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_of_isSome_minKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).minKey?.isSome = true → t.minKey?.isSome = true
-- Init.Data.Bool
Bool.beq_self_left : ∀ (a b : Bool), (a == (a == b)) = b
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- If `F ⋙ G` is full and `G` is faithful, then `F` is full.  -/
CategoryTheory.Functor.Full.of_comp_faithful_iso : ∀ {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} {H : CategoryTheory.Functor C E} [H.Full] [G.Faithful] (h : F.comp G ≅ H), F.Full
-- Mathlib.NumberTheory.Height.NumberField
NumberField.exists_nat_ne_zero_exists_integer_mul_eq_and_absNorm_span_eq_pow : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K),
  ∃ n, n ≠ 0 ∧ ∃ a, ↑n * x = ↑a ∧ Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (Module.finrank ℚ K - 1)
-- Std.Data.DHashMap.Raw
/-- Creates a hash map from an array of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.DHashMap.Raw.ofArray : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Array ((a : α) × β a) → Std.DHashMap.Raw α β