mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A]
  (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C))
  [inst_3 : CategoryTheory.Preadditive A] (X : CategoryTheory.Functor Cᵒᵖ A) (i j : ℕ),
  ((CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor E).obj X).d i j =
    CochainComplex.of.d (fun n => ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op { len := n })).obj i)))
      (AlgebraicTopology.AlternatingCofaceMapComplex.objD
        ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X))
      i j
-- Lean.Declaration
Lean.ConstantInfo.opaqueInfo.injEq : ∀ (val val_1 : Lean.OpaqueVal), (Lean.ConstantInfo.opaqueInfo val = Lean.ConstantInfo.opaqueInfo val_1) = (val = val_1)
-- Mathlib.Data.ENNReal.Operations
ENNReal.image_coe_Iic : ∀ (x : NNReal), ENNReal.ofNNReal '' Set.Iic x = Set.Iic ↑x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize.eq_2 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (v : α → M) (l : ℕ) (f : L.Functions l)
  (ts : Fin l → L.Term α),
  FirstOrder.Language.Term.realize v (FirstOrder.Language.func f ts) =
    FirstOrder.Language.Structure.funMap f fun i => FirstOrder.Language.Term.realize v (ts i)
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.instIsStableUnderCompositionFpqcPrecoverage : AlgebraicGeometry.Scheme.fpqcPrecoverage.IsStableUnderComposition
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.spanningCoe_induce_le : ∀ {V : Type u_1} (G : SimpleGraph V) (s : Set V), (SimpleGraph.induce s G).spanningCoe ≤ G
-- Mathlib.Order.Interval.Multiset
/-- The multiset of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
multiset.  -/
Multiset.Icc : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Multiset α
-- Mathlib.LinearAlgebra.Dual.BaseChange
/-- The linear equivalence underlying `IsBaseChange.dual`.  -/
IsBaseChange.toDualBaseChange : {R : Type u_1} →
  [inst : CommSemiring R] →
    {V : Type u_2} →
      [inst_1 : AddCommMonoid V] →
        [inst_2 : Module R V] →
          {W : Type u_3} →
            [inst_3 : AddCommMonoid W] →
              [inst_4 : Module R W] →
                {A : Type u_4} →
                  [inst_5 : CommSemiring A] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Module A W] →
                        [inst_8 : IsScalarTower R A W] →
                          {j : V →ₗ[R] W} →
                            IsBaseChange A j →
                              [Module.Free R V] →
                                [Module.Finite R V] → TensorProduct R A (Module.Dual R V) ≃ₗ[A] Module.Dual A W
-- Mathlib.FieldTheory.SeparableDegree
IntermediateField.isSeparable_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], Algebra.IsSeparable F ↥⊥
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqErrorCode : BEq Lean.JsonRpc.ErrorCode
-- Std.Data.HashMap.Raw
/-- Two hash maps are equivalent in the sense of `Equiv` iff
all the keys and values are equal.
 -/
Std.HashMap.Raw.Equiv : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → Std.HashMap.Raw α β → Prop
-- Std.Http.Server.Connection
Std.Http.Server.RemoteAddr.mk : Std.Net.SocketAddress → Std.Http.Server.RemoteAddr
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding. Let `e` be a closed embedding of a nonempty topological space `X` into a normal
topological space `Y`. Let `f` be a bounded continuous real-valued function on `X`. Then there
exists a bounded continuous function `g : Y →ᵇ ℝ` such that `g ∘ e = f` and each value `g y` belongs
to a closed interval `[f x₁, f x₂]` for some `x₁` and `x₂`.  -/
BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y] [Nonempty X]
  (f : BoundedContinuousFunction X ℝ) {e : X → Y},
  Topology.IsClosedEmbedding e → ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Set.Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_one : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : One F] [inst_2 : One β]
  [IsOneApply F α β], ⇑1 = 1
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A ring is a simple module over itself iff it is a division ring.  -/
isSimpleModule_self_iff_isUnit : ∀ {R : Type u_2} [inst : Ring R], IsSimpleModule R R ↔ Nontrivial R ∧ ∀ (x : R), x ≠ 0 → IsUnit x
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.Lean.Loop.forIn.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b' : β) (h_1 : (b' : β) → motive (ForInStep.done b'))
  (h_2 : (b' : β) → motive (ForInStep.yield b')),
  (match ForInStep.done b' with
    | ForInStep.done b' => h_1 b'
    | ForInStep.yield b' => h_2 b') =
    h_1 b'
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_of_contains_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α}, (t.erase k).contains a = true → t.contains a = true
-- Mathlib.Algebra.Star.Unitary
/-- `unitary` as a `Subgroup` of a group.

Note the group structure on this type is not defeq to the one on `unitary`.
This situation naturally arises when considering the unitary elements as a
subgroup of the group of units of a star monoid.  -/
unitarySubgroup : (G : Type u_2) → [inst : Group G] → [StarMul G] → Subgroup G
-- Mathlib.Algebra.Order.SuccPred.TypeTags
instIsPredArchimedeanAdditive : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : PredOrder X] [h : IsPredArchimedean X], IsPredArchimedean (Additive X)
-- Mathlib.Topology.CompactOpen
ContinuousMap.tendsto_compactOpen_iff_forall : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {ι : Type u_6} {l : Filter ι}
  (F : ι → C(X, Y)) (f : C(X, Y)),
  Filter.Tendsto F l (nhds f) ↔
    ∀ (K : Set X),
      IsCompact K → Filter.Tendsto (fun i => ContinuousMap.restrict K (F i)) l (nhds (ContinuousMap.restrict K f))
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_le : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖a / b‖ ≤ ‖a‖ + ‖b‖
-- Batteries.Control.ForInStep.Basic
/-- This is similar to a monadic `bind` operator, except that the two type parameters have to be
the same, which prevents putting a monad instance on `ForInStepT m α := m (ForInStep α)`.
 -/
ForInStep.bind : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → ForInStep α → (α → m (ForInStep α)) → m (ForInStep α)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
Submonoid.coe_finsetProd : ∀ {ι : Type u_4} {M : Type u_5} [inst : CommMonoid M] (S : Submonoid M) (f : ι → ↥S) (s : Finset ι),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instStarRingOfStarHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] →
                    [inst_6 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                      [inst_7 : (i : ι) → StarRing (G i)] →
                        [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] → StarRing (DirectLimit G f)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instAdditiveShiftFunctorInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ), (CategoryTheory.shiftFunctor (DerivedCategory C) n).Additive
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.TacticMVarKind.logError : Lean.Syntax → Lean.Elab.Term.TacticMVarKind → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Group.Prod
MonoidHom.coe_snd : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N], ⇑(MonoidHom.snd M N) = Prod.snd
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.saveSplitDiagInfo : Lean.Expr → ℕ → ℕ → Lean.Meta.Grind.SplitSource → Lean.Meta.Grind.GrindM Unit
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.Associative.assoc : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {c₃ : ComplexShape I₃} {c₁₂ : ComplexShape I₁₂} {c₂₃ : ComplexShape I₂₃}
  {c : ComplexShape J} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₁₂ c₃ c}
  {inst_2 : TotalComplexShape c₂ c₃ c₂₃} {inst_3 : TotalComplexShape c₁ c₂₃ c} [self : c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃), c₁₂.π c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.π c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃))
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_neg : ∀ {w i : ℕ} {x : BitVec w}, (-x).getMsbD i = (x.getMsbD i ^^ decide (∃ j < w, i < j ∧ x.getMsbD j = true))
-- Mathlib.Order.Height
Set.chainHeight_mono : ∀ {α : Type u_1} (r : α → α → Prop) (s t : Set α), s ⊆ t → s.chainHeight r ≤ t.chainHeight r
-- Mathlib.Analysis.InnerProductSpace.Defs
HilbertSpace.mk.sizeOf_spec : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] [inst_4 : SizeOf 𝕜] [inst_5 : SizeOf E], sizeOf { } = 1
-- Mathlib.Topology.Order.LeftRightLim
Monotone.tendsto_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f →
    ∀ [inst_4 : TopologicalSpace α] [OrderTopology α] (x : α),
      Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (Function.leftLim f x))
-- Mathlib.Order.Filter.Basic
Filter.sdiff_mem : ∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∈ f → tᶜ ∈ f → s \ t ∈ f
-- Mathlib.Data.Nat.Factors
Nat.mem_primeFactorsList_mul_of_coprime : ∀ {a b : ℕ}, a.Coprime b → ∀ (p : ℕ), p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList
-- Init.Data.BitVec.Lemmas
BitVec.sshiftRight_or_distrib : ∀ {w : ℕ} (x y : BitVec w) (n : ℕ), (x ||| y).sshiftRight n = x.sshiftRight n ||| y.sshiftRight n
-- Mathlib.Order.Monotone.Basic
strictMono_int_of_lt_succ : ∀ {α : Type u} [inst : Preorder α] {f : ℤ → α}, (∀ (n : ℤ), f n < f (n + 1)) → StrictMono f
-- Mathlib.GroupTheory.ArchimedeanDensely
instLocallyFiniteOrderAdditive : {X : Type u_2} → [inst : Preorder X] → [LocallyFiniteOrder X] → LocallyFiniteOrder (Additive X)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_of_mem_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, a ∈ t.insert k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.map_comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (g : B →ₜ* C) (f : A →ₜ* B),
  PontryaginDual.map (g.comp f) = (PontryaginDual.map f).comp (PontryaginDual.map g)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insertMany!_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k},
      List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
        ⟨k, v⟩ ∈ l → ∀ {h' : k' ∈ ↑(t.insertMany! l)}, (↑(t.insertMany! l)).get k' h' = cast ⋯ v
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `G` be a complete nonarchimedean additive abelian group, and let `f : α → G`
be a function that tends to zero on the filter of cofinite sets. Then `f` is unconditionally
summable.  -/
NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G]
  [NonarchimedeanAddGroup G] [CompleteSpace G] {f : α → G}, Filter.Tendsto f Filter.cofinite (nhds 0) → Summable f
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.isIso_g' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C],
  S.Exact → ∀ (h : S.RightHomologyData) [CategoryTheory.Epi S.g], CategoryTheory.IsIso h.g'
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_insertIfNew_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, k ∈ m.insertIfNew k v
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Monotone.linearGrowthInf_comp : ∀ {u : ℕ → EReal} {v : ℕ → ℕ} {a : EReal},
  Monotone u →
    Filter.Tendsto (fun n => ↑(v n) / ↑n) Filter.atTop (nhds a) →
      a ≠ 0 → a ≠ ⊤ → LinearGrowth.linearGrowthInf (u ∘ v) = a * LinearGrowth.linearGrowthInf u
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_Ioc_eq_restrict_Icc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, μ.restrict (Set.Ioc a b) = μ.restrict (Set.Icc a b)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.GradedNatTrans.mk.inj : ∀ {V : Type v} {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁}
  {inst_2 : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst_3 : CategoryTheory.EnrichedCategory V D}
  {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D}
  {app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X}
  {naturality :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y))
            (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y))
          (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))}
  {app_1 : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X}
  {naturality_1 :
    ∀ (X Y : C),
      CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app_1 Y))
            (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app_1 X) (G.map X Y))
          (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))},
  { app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 } → app = app_1
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff_of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.RespectsIso],
  (∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X),
      P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) →
    P.IsLocalAtSource K
-- Mathlib.Logic.Small.Set
small_biUnion : ∀ {α : Type u1} {ι : Type u4} (s : Set ι) [Small.{u, u4} ↑s] (f : (i : ι) → i ∈ s → Set α)
  [∀ (i : ι) (hi : i ∈ s), Small.{u, u1} ↑(f i hi)], Small.{u, u1} ↑(⋃ i, ⋃ (hi : i ∈ s), f i hi)
-- Mathlib.Data.Finset.Defs
Finset.not_subset : ∀ {α : Type u_1} {s t : Finset α}, ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t
-- Mathlib.Topology.NhdsWithin
Filter.EventuallyEq.mem_interior_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s t : Set α}, s =ᶠ[nhds x] t → (x ∈ interior s ↔ x ∈ interior t)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.DocumentHighlightParams
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.curryRingEquiv_single : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (m : M)
  (n : N) (r : R),
  MonoidAlgebra.curryRingEquiv (MonoidAlgebra.single (m, n) r) = MonoidAlgebra.single m (MonoidAlgebra.single n r)
-- Init.Data.Fin.Lemmas
Fin.rev_zero : ∀ (n : ℕ), Fin.rev 0 = Fin.last n
-- Init.Data.Array.Basic
Array.toArrayAux_eq : ∀ {α : Type u} {as : List α} {acc : Array α}, (as.toArrayAux acc).toList = acc.toList ++ as
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {l : List α} {k : α}, k ∈ t → (t.insertMany l).get! k = t.get! k
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Algebra.isIntegral_of_surjective : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B],
  Function.Surjective ⇑(algebraMap R B) → Algebra.IsIntegral R B
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofHasPullback_π : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃) [inst_3 : CategoryTheory.Limits.HasPullback ((G.obj (Opposite.op X₁)).map f₃) ((G.map f₁.op).app Y₃)],
  (CategoryTheory.Functor.PullbackObjObj.ofHasPullback G f₁ f₃).π =
    CategoryTheory.Limits.pullback.lift ((G.map f₁.op).app X₃) ((G.obj (Opposite.op Y₁)).map f₃) ⋯
-- Mathlib.Analysis.ODE.PicardLindelof
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, integral form. This version shows the existence
of a local solution whose initial point `x` may be different from the centre `x₀` of the closed
ball within which the properties of the vector field hold.  -/
IsPicardLindelof.exists_eq_forall_mem_Icc_eq_picard : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E}
  {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    x ∈ Metric.closedBall x₀ ↑r → ∃ α, α ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, α t = ODE.picard f (↑t₀) x α t
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapEquiv_apply : ∀ {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [inst : CommSemiring S₁] [inst_1 : CommSemiring S₂] (e : S₁ ≃+* S₂)
  (x : MvPolynomial σ S₁), (MvPolynomial.mapEquiv σ e) x = (MvPolynomial.map ↑e) x
-- Mathlib.Data.Nat.Count
Nat.count_iff_forall : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, Nat.count p n = n ↔ ∀ n' < n, p n'
-- Init.Data.BitVec.Lemmas
BitVec.udiv_eq_and : ∀ {x y : BitVec 1}, x / y = x &&& y
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The `C : R → R[X₁, ..., Xₘ]` case of **Chevalley's theorem** with complexity bound.  -/
ChevalleyThm.chevalley_mvPolynomialC : ∀ {R : Type u_2} [inst : CommRing R] {n : ℕ} {M : Submodule ℤ R},
  1 ∈ M →
    ∀ (k : ℕ) (d : Multiset (Fin n)) (S : PrimeSpectrum.ConstructibleSetData (MvPolynomial (Fin n) R)),
      (∀ C ∈ S, C.n ≤ k) →
        (∀ C ∈ S,
            ∀ (j : Fin C.n),
              C.g j ∈
                MvPolynomial.coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (MvPolynomial.degreesLE R (Fin n) d)) →
          ∃ T,
            PrimeSpectrum.comap MvPolynomial.C '' S.toSet = T.toSet ∧
              ∀ C ∈ T,
                C.n ≤ ChevalleyThm.MvPolynomialC.numBound k (fun i => 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                  ∀ (i : Fin C.n),
                    C.g i ∈
                      M ^
                        ChevalleyThm.MvPolynomialC.degBound k (fun i => 1 + Multiset.count i (Multiset.map Fin.val d)) n
-- Mathlib.MeasureTheory.Group.Convolution
/-- Multiplicative convolution of measures.  -/
MeasureTheory.Measure.mconv : {M : Type u_1} →
  [Monoid M] → [inst : MeasurableSpace M] → MeasureTheory.Measure M → MeasureTheory.Measure M → MeasureTheory.Measure M
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.ExceptT.bindCont.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is equicontinuous at some `x₀ : X`, then the limit is continuous at `x₀`.  -/
Filter.Tendsto.continuousAt_of_equicontinuousAt : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι} [l.NeBot]
  {F : ι → X → α} {f : X → α} {x₀ : X}, Filter.Tendsto F l (nhds f) → EquicontinuousAt F x₀ → ContinuousAt f x₀
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.maxVar_bound : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {x y : X ⊕ Y} [CompactSpace X] [Nonempty X]
  [CompactSpace Y] [Nonempty Y], dist x y ≤ ↑(GromovHausdorff.maxVar✝ X Y)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ (l : List α), m₁.Equiv m₂ → (m₁.insertMany l).Equiv (m₂.insertMany l)
-- Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
/-- If `c₁` and `c₂` are colimit cofans and `bc` is a colimit binary cofan on their cocone
points, then the cofan constructed from `combPairHoms` is a colimit cocone.  -/
CategoryTheory.Limits.Cofan.combPairIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {ι₁ : Type u_1} →
      {ι₂ : Type u_2} →
        {f₁ : ι₁ → C} →
          {f₂ : ι₂ → C} →
            {c₁ : CategoryTheory.Limits.Cofan f₁} →
              {c₂ : CategoryTheory.Limits.Cofan f₂} →
                {bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt} →
                  CategoryTheory.Limits.IsColimit c₁ →
                    CategoryTheory.Limits.IsColimit c₂ →
                      CategoryTheory.Limits.IsColimit bc →
                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk bc.pt (c₁.combPairHoms c₂ bc))
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.opaque.sizeOf_spec : sizeOf Lean.ExternEntry.opaque = 1
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
CategoryTheory.Limits.Types.mono_inl : ∀ {S X₁ X₂ : Type u} {f : S ⟶ X₁} {g : S ⟶ X₂} [CategoryTheory.Mono g],
  CategoryTheory.Mono (CategoryTheory.Limits.Types.Pushout.inl f g)