mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Mul
IsStablyFiniteRing.mk : ∀ {R : Type u_10} [inst : MulOne R] [inst_1 : AddCommMonoid R],
  (∀ (n : ℕ), IsDedekindFiniteMonoid (Matrix (Fin n) (Fin n) R)) → IsStablyFiniteRing R
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instIsRightCancelMulOfMulOpposite : ∀ {M : Type u_1} [inst : Mul Mᵐᵒᵖ] [IsRightCancelMul Mᵐᵒᵖ], IsRightCancelMul Mᵈᵐᵃ
-- Std.Do.Triple.SpecLemmas
control.eq_1 : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : MonadControlT m n] [inst_1 : Bind n] {α : Type u}
  (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)), control f = controlAt m f
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.card_four : ∀ {G : Type u_1} {inst : AddGroup G} [self : IsAddKleinFour G], Nat.card G = 4
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A}
  (H : g.IsWeierstrassFactorizationAt f h I) [inst_1 : IsAdicComplete I A] (a : Polynomial A ⧸ Ideal.span {f}),
  H.algEquivQuotient a =
    (Ideal.quotientEquivAlgOfEq A ⋯) ((Ideal.quotientMapₐ (Ideal.span {↑f}) (Polynomial.coeToPowerSeries.algHom A) ⋯) a)
-- Mathlib.Combinatorics.Additive.Energy
/-- The additive energy of a finset `s` in a group is the number of quadruples
`(a₁, a₂, b₁, b₂) ∈ s × s × s × s` such that `a₁ + b₁ = a₂ + b₂`.  -/
Combinatorics.Additive.«termE[_]» : Lean.ParserDescr
-- Mathlib.Data.Nat.Digits.Defs
/-- `ofDigits b L` takes a list `L` of natural numbers, and interprets them
as a number in semiring, as the little-endian digits in base `b`.
 -/
Nat.ofDigits : {α : Type u_1} → [Semiring α] → α → List ℕ → α
-- Mathlib.CategoryTheory.Yoneda
/-- `FullyFaithful.homEquiv` as a natural isomorphism.  -/
CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          F.FullyFaithful →
            (F.comp
                (CategoryTheory.uliftYoneda.{v₁, v₂, u₂}.comp
                  ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op)) ≅
              CategoryTheory.uliftYoneda.{v₂, v₁, u₁})
-- Mathlib.Data.Finmap
/-- Multiset of keys of an association multiset.  -/
Multiset.keys : {α : Type u} → {β : α → Type v} → Multiset (Sigma β) → Multiset α
-- Mathlib.NumberTheory.ModularForms.BoundedAtCusp
/-- We say `f` is zero at `c` if, for all `g` with `g • ∞ = c`, the function `f ∣[k] g` is
zero at `∞`.  -/
OnePoint.IsZeroAt : OnePoint ℝ → (UpperHalfPlane → ℂ) → ℤ → Prop
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] {n : ℕ} (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))}
  {m : ℕ} (h : fs.card = m + 1) {w : Fin (n + 1) → k},
  ∑ i, w i = 1 →
    ((Finset.affineCombination k Finset.univ s.points) w ∈ (s.face h).closedInterior ↔
      (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionalIdeal.mul_right_strictMono : ∀ {A : Type u_2} (K : Type u_3) [inst : CommRing A] [inst_1 : Field K] [IsDedekindDomain A] [inst_3 : Algebra A K]
  [IsFractionRing A K] {I : FractionalIdeal (nonZeroDivisors A) K}, I ≠ 0 → StrictMono fun x => I * x
-- Mathlib.Topology.UniformSpace.Cauchy
complete_of_compact : ∀ {α : Type u} [inst : UniformSpace α] [CompactSpace α], CompleteSpace α
-- Lean.Expr
Lean.instBEqLiteral : BEq Lean.Literal
-- Mathlib.Topology.Instances.ENat
ENat.instIsTopologicalSemiring : IsTopologicalSemiring ℕ∞
-- Mathlib.Analysis.InnerProductSpace.Adjoint
Unitary.coe_symm_linearIsometryEquiv_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] (e : H ≃ₗᵢ[𝕜] H), ↑(Unitary.linearIsometryEquiv.symm e) = ↑↑e
-- Mathlib.RingTheory.Nilpotent.Basic
isNilpotent_neg_iff : ∀ {R : Type u_1} {x : R} [inst : Ring R], IsNilpotent (-x) ↔ IsNilpotent x
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `u₁` and `u₂` are two uniform structures on `γ`, then
`𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂)`.  -/
UniformOnFun.inf_eq : ∀ {α : Type u_1} {γ : Type u_3} {𝔖 : Set (Set α)} {u₁ u₂ : UniformSpace γ},
  UniformOnFun.uniformSpace α γ 𝔖 = UniformOnFun.uniformSpace α γ 𝔖 ⊓ UniformOnFun.uniformSpace α γ 𝔖
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_carrier : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : L.Substructure M} {x : M}, x ∈ ↑s ↔ x ∈ s
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : SizeOf α] (carrier : Set α) (isClopen' : IsClopen carrier),
  sizeOf { carrier := carrier, isClopen' := isClopen' } = 1 + sizeOf isClopen'
-- Batteries.Tactic.Lemma
/-- Elaborator for the `lemma` command, if the option `lang.lemmaCmd` is false the command
emits a warning and code action instructing the user to use `theorem` instead. -/
Batteries.Tactic.Lemma.elabLemma : Lean.Elab.Command.CommandElab
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.instInhabitedSplittingField : {K : Type u_1} → [inst : Field K] → (f : Polynomial K) → Inhabited f.SplittingField
-- Mathlib.Algebra.Order.Monoid.Units
Units.instMinOfLinearOrder.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : LinearOrder α],
  Units.instMinOfLinearOrder = { min := fun a b => if a ≤ b then a else b }
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.instPreservesFiniteColimitsObjFunctorRightExactFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ᵣ D), CategoryTheory.Limits.PreservesFiniteColimits F.obj
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_eq_minD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.min! = t.minD default
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.isLinearOrder : Lean.Meta.Grind.Arith.Linear.LinearM Bool
-- Mathlib.RingTheory.Artinian.Defs
isArtinianRing_iff : ∀ {R : Type u_1} [inst : Semiring R], IsArtinianRing R ↔ IsArtinian R R
-- Mathlib.Data.Nat.Cast.Basic
Nat.cast_id : ∀ (n : ℕ), ↑n = n
-- Mathlib.Order.ModularLattice
/-- A weakly lower modular lattice is a lattice where `a` and `b` cover `a ⊓ b` if `a ⊔ b` covers
both `a` and `b`.  -/
IsWeakLowerModularLattice : (α : Type u_2) → [Lattice α] → Prop
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.GeometricallyReduced.eq_geometrically : @AlgebraicGeometry.GeometricallyReduced = AlgebraicGeometry.geometrically AlgebraicGeometry.IsReduced
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_Ioi_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] {a : α} {f : β → ↑(Set.Ioi a)} {l : Filter β},
  Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun x => ↑(f x)) l Filter.atTop
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.instInhabitedMCasesPat : Inhabited Lean.Parser.Tactic.MCasesPat
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.TreeMap.minEntry! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap α β cmp → α × β
-- Mathlib.CategoryTheory.Limits.Connected
/-- If `J` is connected, `F : J ⥤ C` and `C` is a cocone on `F`, then to check that `c` is a
colimit it is sufficient to check that `colimMap c.ι` is an isomorphism. The converse is also
true, see `Cocone.isColimit_iff_isIso_colimMap_ι`.  -/
CategoryTheory.Limits.Cocone.isColimitOfIsIsoColimMapι : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        [inst_2 : CategoryTheory.IsConnected J] →
          {F : CategoryTheory.Functor J C} →
            [inst_3 : CategoryTheory.Limits.HasColimit F] →
              (c : CategoryTheory.Limits.Cocone F) →
                [CategoryTheory.IsIso (CategoryTheory.Limits.colimMap c.ι)] → CategoryTheory.Limits.IsColimit c
-- Mathlib.GroupTheory.RegularWreathProduct
IteratedWreathProduct_zero : ∀ (G : Type u), IteratedWreathProduct G 0 = PUnit.{u + 1}
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- "Trivial Square-Zero Extension".

Given a module `M` over a ring `R`, the trivial square-zero extension of `M` over `R` is defined
to be the `R`-algebra `R × M` with multiplication given by
`(r₁ + m₁) * (r₂ + m₂) = r₁ r₂ + r₁ m₂ + r₂ m₁`.

It is a square-zero extension because `M^2 = 0`.
 -/
TrivSqZeroExt : Type u → Type v → Type (max u v)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
there is a linear map `LocalizedModule S M → M''`.
 -/
LocalizedModule.lift : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M'' : Type u_4} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M''] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M''] →
                  (M →ₗ[R] M'') →
                    (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → LocalizedModule S M →ₗ[R] M''
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
/-- The functor `opFunctor : SimplicialObject C ⥤ SimplicialObject C`
is a covariant involution.  -/
SimplicialObject.opFunctorCompOpFunctorIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    SimplicialObject.opFunctor.comp SimplicialObject.opFunctor ≅
      CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C)
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.Candidate.kind : Lean.Server.FileWorker.SignatureHelp.Candidate → Lean.Server.FileWorker.SignatureHelp.CandidateKind
-- Init.Data.Int.Order
Int.not_le_of_gt : ∀ {a b : ℤ}, b < a → ¬a ≤ b
-- Mathlib.Order.BooleanAlgebra.Basic
compl_eq_iff_isCompl : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], xᶜ = y ↔ IsCompl x y
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.autMap_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected X] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois Y]
  [inst_4 : CategoryTheory.PreGaloisCategory.IsGalois Z] (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.PreGaloisCategory.autMap (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.PreGaloisCategory.autMap g ∘ CategoryTheory.PreGaloisCategory.autMap f
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalFocus : Lean.Elab.Tactic.Tactic
-- Batteries.Data.List.Basic
List.swap.eq_4 : ∀ {α : Type u_1} (a : α) (xs : List α) (i : ℕ), (a :: xs).swap i.succ 0 = xs[i]?.getD a :: xs.set i a
-- Mathlib.Data.Subtype
/-- An alternative version of `Subtype.forall`. This one is useful if Lean cannot figure out `q`
when using `Subtype.forall` from right to left.  -/
Subtype.forall' : ∀ {α : Sort u_1} {p : α → Prop} {q : (x : α) → p x → Prop}, (∀ (x : α) (h : p x), q x h) ↔ ∀ (x : { a // p a }), q ↑x ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.keyAtIdxD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.keyAtIdxD i fallback = t₂.keyAtIdxD i fallback
-- Lean.Parser.Command
Lean.Parser.Command.openRenamingItem.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} (Y : AlgebraicGeometry.SheafedSpace C)
  {f : X ⟶ ↑Y.toPresheafedSpace} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion (Y.ofRestrict hf)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.commShiftIso_hom_naturality : ∀ {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 : CategoryTheory.Functor C D) {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] {X Y : C}
  (f : X ⟶ Y) (a : A),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f))
      ((CategoryTheory.Functor.commShiftIso F a).hom.app Y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
      ((CategoryTheory.shiftFunctor D a).map (F.map f))
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {kf : CategoryTheory.Limits.KernelFork S.g}
  (hkf : CategoryTheory.Limits.IsLimit kf),
  CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).hom S.iCycles = CategoryTheory.Limits.Fork.ι kf
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        k ∉ m₂ → Std.DHashMap.Raw.Const.getD (m₁.diff m₂) k fallback = Std.DHashMap.Raw.Const.getD m₁ k fallback
-- Mathlib.Tactic.Translate.GuessName
_private.Mathlib.Tactic.Translate.GuessName.0.Mathlib.Tactic.GuessName.fixAbbreviationAux.match_3.eq_2 : ∀ (motive : List String → List String → Sort u_1) (x : String) (s : List String) (h_1 : Unit → motive [] [])
  (h_2 : (x : String) → (s : List String) → motive [] (x :: s))
  (h_3 : (pre : String) → (l s' : List String) → motive (pre :: l) s'),
  (match [], x :: s with
    | [], [] => h_1 ()
    | [], x :: s => h_2 x s
    | pre :: l, s' => h_3 pre l s') =
    h_2 x s
-- Lean.Syntax
Lean.instBEqSourceInfo_lean : BEq Lean.SourceInfo
-- Mathlib.Analysis.Convex.Cone.InnerDual
ProperCone.innerDual_empty : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : CompleteSpace E],
  ProperCone.innerDual ∅ = ⊤
-- Mathlib.Computability.Ackermann
_private.Mathlib.Computability.Ackermann.0.ack.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (m : ℕ) (h_1 : (n : ℕ) → motive 0 n) (h_2 : (m : ℕ) → motive m.succ 0)
  (h_3 : (m n : ℕ) → motive m.succ n.succ),
  (match m.succ, 0 with
    | 0, n => h_1 n
    | m.succ, 0 => h_2 m
    | m.succ, n.succ => h_3 m n) =
    h_2 m
-- Lean.Declaration
/-- Constructor index (i.e., Position in the inductive declaration)  -/
Lean.ConstructorVal.cidx : Lean.ConstructorVal → ℕ
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
/-- If `M` is a submodule in an algebra `S` over `R`, there is the natural `R`-linear map
`M ⊗[R] i(R) →ₗ[R] M` induced by multiplication in `S`, here `i : R → S` is the structure map.
This is promoted to an isomorphism of `R`-modules as `Submodule.rTensorOne`. Use that instead.  -/
Submodule.rTensorOne' : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (M : Submodule R S) → TensorProduct R ↥M ↥⊥ →ₗ[R] ↥M
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ofComp.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι),
  Q.ofComp P = { val := fun i => Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val) i, aeval_val := ⋯ }
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.simpOnlyBuiltins : List Lean.Name
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k a : α} {fallback : β a} {v : β k},
      (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- (Implementation) The natural map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_X, 𝖣.ι i '' U)`.
This forms the inverse of `(𝖣.ι i).c.app (op U)`.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : AlgebraicGeometry.PresheafedSpace.GlueData C) →
      [inst_1 : CategoryTheory.Limits.HasLimits C] →
        {i : D.J} →
          (U : TopologicalSpace.Opens ↑↑(D.U i)) →
            (D.U i).presheaf.obj (Opposite.op U) ⟶ CategoryTheory.Limits.limit (D.diagramOverOpen U)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_def : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
  G.neighborFinset v = (G.neighborSet v).toFinset
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_insertEntryIfNew_le_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α},
        (compare (Std.Internal.List.minKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback)
              (Std.Internal.List.minKeyD l fallback)).isLE =
          true
-- Mathlib.Analysis.Calculus.DifferentialForm.VectorField
/-- If `ω` is a differentiable `(n + 1)`-form and `V i` are `n + 2` differentiable vector fields, then

$$
  dω(V_0(x), \dots, V_{n + 1}(x)) =
    \sum_{i=0}^{n + 1} (-1)^i •
      D_x\left(ω\big(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)\big)\right)(V_i(x)) -
      \sum_{0 \le i \le j\le n} (-1)^{i + j}
        ω\big(x; [V_i, V_{j + 1}](x),
          V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_{j + 1}(x)}, …, V_k(x)\big),
$$

where $[V_i, V_{j + 1}]$ is the commutator of the vector fields $V_i$ and $V_{j + 1}$.
As usual, $\widehat{V_i(x)}$ means that this item is removed from the sequence.

In informal texts, this formula is usually written as

$$
  dω(V_0(x), \dots, V_{n + 1}(x)) =
    \sum_{i=0}^{n + 1} (-1)^i •
      D_x\left(ω\big(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)\big)\right)(V_i(x)) -
      \sum_{0 \le i < j\le n + 1} (-1)^{i + j}
        ω\big(x; [V_i, V_j](x),
          V_0(x), …, \widehat{V_i(x)}, …, \widehat{V_j(x)}, …, V_k(x)\big).
$$

In the sum from our formalization,
each index `(i, j)` corresponds to the index `(Fin.castSucc i, Fin.succ j)`
in the sum used in informal texts.

For this reason, `i + j` in our sum has the opposite parity compared to informal texts,
which changes the sign before the sum from `+` to `-`.
 -/
extDeriv_apply_vectorField : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {x : E}
  {ω : E → E [⋀^Fin (n + 1)]→L[𝕜] F} {V : Fin (n + 2) → E → E},
  DifferentiableAt 𝕜 ω x →
    (∀ (i : Fin (n + 2)), DifferentiableAt 𝕜 (V i) x) →
      ((extDeriv ω x) fun x_1 => V x_1 x) =
        ∑ i, (-1) ^ ↑i • (fderiv 𝕜 (fun x => (ω x) (i.removeNth fun x_1 => V x_1 x)) x) (V i x) -
          ∑ i,
            ∑ j ≥ i,
              (-1) ^ (↑i + ↑j) •
                (ω x)
                  (Matrix.vecCons (VectorField.lieBracket 𝕜 (V i.castSucc) (V j.succ) x)
                    (j.removeNth (i.castSucc.removeNth fun x_1 => V x_1 x)))
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_lt_toNNReal_iff : ∀ {r p : ℝ}, 0 < p → (r.toNNReal < p.toNNReal ↔ r < p)
-- Mathlib.Topology.Order.IsLocallyClosed
isLocallyClosed_Ioi : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a : X} [inst_1 : LinearOrder X] [ClosedIicTopology X],
  IsLocallyClosed (Set.Ioi a)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (y : ↥Y),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap e.hom (e.inv y))
      (AlgebraicGeometry.Scheme.Hom.stalkMap e.inv y) =
    (Y.presheaf.stalkCongr ⋯).hom
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getValueCast? : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [LawfulBEq α] → (a : α) → List ((a : α) × β a) → Option (β a)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_hadamard_one : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α], (SimpleGraph.adjMatrix α G).hadamard 1 = 0
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- Function multiplied by the inverse of its p-seminorm `(∫⁻ f^p ∂μ) ^ 1/p`  -/
ENNReal.funMulInvSnorm : {α : Type u_1} → [inst : MeasurableSpace α] → (α → ENNReal) → ℝ → MeasureTheory.Measure α → α → ENNReal
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Construct a term of `ProfiniteGrp` from a type endowed with the structure of a
profinite topological group.  -/
ProfiniteGrp.ofProfinite : (G : Profinite) → [inst : Group ↑G.toTop] → [IsTopologicalGroup ↑G.toTop] → ProfiniteGrp.{u_1}
-- Init.Data.List.Attach
List.countP_attach : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, List.countP (fun a => p ↑a) l.attach = List.countP p l
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_inter_inter : ∀ {α : Type u_1} (t s₁ s₂ s₁' s₂' : Set α), t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'
-- Mathlib.Data.Stream.Init
Stream'.get.eq_1 : ∀ {α : Type u} (s : Stream' α) (n : ℕ), s.get n = s n
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The Lévy-Prokhorov distance `levyProkhorovEDist` makes `Measure Ω` a pseudoemetric
space. The instance is recorded on the type synonym `LevyProkhorov (Measure Ω) := Measure Ω`.  -/
MeasureTheory.LevyProkhorov.instPseudoEMetricSpaceMeasure : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : PseudoEMetricSpace Ω] →
      [OpensMeasurableSpace Ω] → PseudoEMetricSpace (MeasureTheory.LevyProkhorov (MeasureTheory.Measure Ω))
-- Init.Data.SInt.Basic
/-- Converts a 16-bit signed integer to a natural number, mapping all negative numbers to `0`.

Use `Int16.toBitVec` to obtain the two's complement representation.
 -/
Int16.toNatClampNeg : Int16 → ℕ
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- The saturation of a submonoid `s` is the intersection of all saturated submonoids that contain
`s`.

If `M` is a commutative monoid, then this is `{x : M | ∃ y : M, x * y ∈ s}`.  -/
Submonoid.saturation : {M : Type u_1} → [inst : MulOneClass M] → Submonoid M → SaturatedSubmonoid M
-- Mathlib.Algebra.Group.TransferInstance
Equiv.monoid.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Monoid β], e.monoid = Function.Injective.monoid ⇑e ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
/-- The functor `AddCommGrpCat ⥤ CommGrpCat` by sending `X ↦ Multiplicative X` and `f ↦ f`.
 -/
AddCommGrpCat.toCommGrp : CategoryTheory.Functor AddCommGrpCat CommGrpCat
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The type family of morphisms for the diagram indexing a (co)equalizer.  -/
CategoryTheory.Limits.WalkingParallelPairHom : CategoryTheory.Limits.WalkingParallelPair → CategoryTheory.Limits.WalkingParallelPair → Type
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edge_le : ∀ {V : Type u_1} (G : SimpleGraph V) (s t : V), SimpleGraph.edge s t ≤ G ↔ {s(s, t)} \ Sym2.diagSet ⊆ G.edgeSet
-- Lean.Data.JsonRpc
/-- A string providing a short description of the error.  -/
Lean.JsonRpc.ResponseError.message : {α : Type u} → Lean.JsonRpc.ResponseError α → String