mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.modifyCommRing : (Lean.Meta.Grind.Arith.CommRing.CommRing → Lean.Meta.Grind.Arith.CommRing.CommRing) →
  Lean.Meta.Grind.Arith.CommRing.RingM Unit
-- Init.Data.Array.Lemmas
Array.flatMap_toArray : ∀ {α : Type u_1} {β : Type u_2} {f : α → Array β} {as : List α},
  Array.flatMap f as.toArray = (List.flatMap (fun a => (f a).toList) as).toArray
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- Let `E`, `F` be two Hausdorff topological vector spaces over a complete `NontriviallyNormedField`
denoted `𝕜`, and `u : E →L[𝕜] F` a continuous linear map. The following conditions are equivalent:

1. `u` is a **Fredholm operator**, in the sense of `ContinuousLinearMap.IsFredholm`.
2. `u` admits a continuous **quasi-inverse**, in the sense of `LinearMap.IsQuasiInverse`.
3. There are closed finite-codimension subspaces `E₁` and `F₁` of `E` and `F` between which `u`
  induces an isomorphism.
4. `u` admits a `FredholmPackage`.

In practice, condition `4` is the "strongest", so you should probably not use it to *prove* that an
operator is Fredholm.
 -/
ContinuousLinearMap.isFredholm_tfae : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space E] [T2Space F] (u : E →L[𝕜] F),
  [u.IsFredholm, ∃ v, (↑v).IsQuasiInverse ↑u,
      ∃ E₁ F₁,
        IsClosed ↑E₁ ∧ IsClosed ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : Set.MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible,
      Nonempty u.FredholmPackage].TFAE
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.map.unique : ∀ {α : Type u} {β : Type v} {f : α → β} (g : FreeAddGroup α →+ FreeAddGroup β),
  (∀ (x : α), g (FreeAddGroup.of x) = FreeAddGroup.of (f x)) → ∀ {x : FreeAddGroup α}, g x = (FreeAddGroup.map f) x
-- Mathlib.Data.List.TFAE
List.tfae_not_iff : ∀ {l : List Prop}, (List.map Not l).TFAE ↔ l.TFAE
-- Mathlib.Tactic.CrossRefAttribute
/-- The parenthesizer for LMFDB identifier syntax.  -/
Lean.PrettyPrinter.Parenthesizer.lmfdbIdAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- A sheaf of modules is finitely presented if it is locally the cokernel of a
morphism between coproducts of finitely many copies of the sheaf of rings.  -/
SheafOfModules.IsFinitePresentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] → SheafOfModules R → Prop
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.normalize_content : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p : Polynomial R},
  normalize p.content = p.content
-- Mathlib.Algebra.Lie.TraceForm
LieIdeal.toSubmodule_killingCompl : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  ↑(LieIdeal.killingCompl R L I) = (killingForm R L).orthogonal ↑I
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A category with finite biproducts has binary biproducts.

This is not an instance as typically in concrete categories there will be
an alternative construction with nicer definitional properties.  -/
CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts : ∀ (C : Type uC) [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C], CategoryTheory.Limits.HasBinaryBiproducts C
-- Mathlib.Probability.Process.Adapted
MeasureTheory.isStronglyProgressive_of_tendsto : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : MeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β] {U : ℕ → ι → Ω → β},
  (∀ (l : ℕ), MeasureTheory.IsStronglyProgressive f (U l)) →
    Filter.Tendsto U Filter.atTop (nhds u) → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_toAddSubgroup_eq_zmultiples : ∀ (a : ℤ), Submodule.toAddSubgroup (Ideal.span {a}) = AddSubgroup.zmultiples a
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φQ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).Q
-- Mathlib.Data.List.Permutation
List.nodup_permutations : ∀ {α : Type u_1} (s : List α), s.Nodup → s.permutations.Nodup
-- Mathlib.Data.Fin.SuccPredOrder
Fin.instPredOrder : {n : ℕ} → PredOrder (Fin n)
-- Lean.Data.DeclarationRange
Lean.DeclarationRange.mk : Lean.Position → ℕ → Lean.Position → ℕ → Lean.DeclarationRange
-- Mathlib.Combinatorics.SetFamily.LYM
/-- The shadow of `falling m 𝒜` is disjoint from the `n`-sized elements of `𝒜`, thanks to the
antichain property.  -/
Finset.IsAntichain.disjoint_slice_shadow_falling : ∀ {α : Type u_2} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {m n : ℕ},
  IsAntichain (fun x1 x2 => x1 ⊆ x2) ↑𝒜 → Disjoint (𝒜.slice m) (Finset.falling n 𝒜).shadow
-- Mathlib.RingTheory.Localization.Integral
IsIntegral.exists_multiple_integral_of_isLocalization : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {Rₘ : Type u_3} [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] [IsLocalization M Rₘ] [inst_6 : Algebra Rₘ S]
  [IsScalarTower R Rₘ S] (x : S), IsIntegral Rₘ x → ∃ m, IsIntegral R (m • x)
-- Init.Data.Vector.MapIdx
Vector.mapIdx_eq_append_iff : ∀ {α : Type u_1} {n m : ℕ} {β : Type u_2} {xs : Vector α (n + m)} {f : ℕ → α → β} {ys : Vector β n} {zs : Vector β m},
  Vector.mapIdx f xs = ys ++ zs ↔
    ∃ ys' zs', xs = ys' ++ zs' ∧ Vector.mapIdx f ys' = ys ∧ Vector.mapIdx (fun i => f (i + n)) zs' = zs
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.instFunLikeCompactsENNReal : {G : Type w} → [inst : TopologicalSpace G] → FunLike (MeasureTheory.Content G) (TopologicalSpace.Compacts G) ENNReal
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.instIsGCDMonoid : ∀ {R : Type u_1} [inst : CommRing R] [IsGCDMonoid R], IsGCDMonoid (Polynomial R)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_smul_right_image : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t : Set β}, ⋃ a ∈ t, (fun x => x • a) '' s = s • t
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.forget_createsLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget MonCat)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.cases.inj : ∀ {declName : Lean.Name} {eager : Bool} {declName_1 : Lean.Name} {eager_1 : Bool},
  Lean.Meta.Grind.Entry.cases declName eager = Lean.Meta.Grind.Entry.cases declName_1 eager_1 →
    declName = declName_1 ∧ eager = eager_1
-- Mathlib.ModelTheory.Topology.Types
_private.Mathlib.ModelTheory.Topology.Types.0.CompleteType.instBaireSpaceCompleteType : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1}, BaireSpace (T.CompleteType α)
-- Mathlib.ModelTheory.Definability
/-- A function from a Cartesian power of a structure to that structure is term-definable over
a set `A` when the value of the function is given by a term with constants `A`.  -/
Set.TermDefinable : {M : Type w} → Set M → (L : FirstOrder.Language) → [L.Structure M] → {α : Type u₁} → ((α → M) → M) → Prop
-- Lean.Parser.Types
Lean.Parser.InputContext.not_atEnd_inputString : ∀ {c : Lean.Parser.InputContext} {p : String.Pos.Raw}, ¬c.atEnd p = true → ¬String.Pos.Raw.atEnd c.inputString p = true
-- Mathlib.Data.Set.Pairwise.Basic
Std.Symm.pairwise_on : ∀ {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} [inst : LinearOrder ι] [Std.Symm r] (f : ι → α),
  Pairwise (Function.onFun r f) ↔ ∀ ⦃m n : ι⦄, m < n → r (f m) (f n)
-- Mathlib.Topology.ContinuousMap.Bounded.Star
BoundedContinuousFunction.instCStarRing : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing β] [inst_2 : StarRing β]
  [inst_3 : CStarRing β], CStarRing (BoundedContinuousFunction α β)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.instCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → CategoryTheory.Category.{max v u_2, max (max u v) (u_2 + 1)} (CategoryTheory.PreOneHypercover S)
-- Mathlib.Algebra.Order.Sub.Defs
/-- A more general version of the reverse direction of `sub_eq_sub_iff_add_eq_add`  -/
tsub_eq_tsub_of_add_eq_add : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c d : α}
  [AddLeftReflectLE α], a + d = c + b → a - b = c - d
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- The name length of the used lemma.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.nameLength : Mathlib.Tactic.ClickSuggestions.ApplyAtKey → ℕ
-- Mathlib.Algebra.Order.Hom.Basic
le_map_add_map_div : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommMagma β]
  [inst_3 : LE β] [MulLEAddHomClass F α β] (f : F) (a b : α), f a ≤ f b + f (a / b)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.updateDec! : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu →
    Lean.FVarId → ℕ → Bool → Bool → Option ℕ → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Probability.Process.Predictable
_private.Mathlib.Probability.Process.Predictable.0.MeasureTheory.IsStronglyPredictable.of_measurable_add_one.match_1_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  x = 0 →
    (match x with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_1 ()
-- Mathlib.Algebra.Category.CommAlgCat.Basic
commAlgCatEquivUnder_inverse_map : ∀ (R : CommRingCat) {A B : CategoryTheory.Under R} (f : A ⟶ B),
  (commAlgCatEquivUnder R).inverse.map f = CommAlgCat.ofHom (CommRingCat.toAlgHom f)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOf_self : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.addSubgroupOf H = ⊤
-- Mathlib.Order.BooleanAlgebra.Set
Set.notMem_compl_iff : ∀ {α : Type u_1} {s : Set α} {x : α}, x ∉ sᶜ ↔ x ∈ s
-- Mathlib.Topology.UniformSpace.Uniformizable
CompletelyRegularSpace.of_exists_uniformSpace : ∀ {X : Type u_1} [t : TopologicalSpace X], (∃ u, u.toTopologicalSpace = t) → CompletelyRegularSpace X
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
/-- If `μ univ < n * μ s` and `f` is a map preserving measure `μ`,
then for some `x ∈ s` and `0 < m < n`, `f^[m] x ∈ s`.  -/
MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → α} {s : Set α},
  MeasureTheory.MeasurePreserving f μ μ →
    MeasureTheory.NullMeasurableSet s μ → ∀ {n : ℕ}, μ Set.univ < ↑n * μ s → ∃ x ∈ s, ∃ m ∈ Set.Ioo 0 n, f^[m] x ∈ s
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
CommGrpCat.toAddCommGrp_obj_coe : ∀ (X : CommGrpCat), ↑(CommGrpCat.toAddCommGrp.obj X) = Additive ↑X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertIfNew! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {v : β}
  {h₁ : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) a h₁ =
    if h₂ : compare k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Internal.Impl.Const.get t a ⋯
-- Lean.Structure
/-- Returns the constructor of the structure named `constName` if it is a non-recursive single-constructor inductive type with no indices.
 -/
Lean.getNonRecStructureCtor? : Lean.Environment → Lean.Name → Option Lean.ConstructorVal
-- Mathlib.Algebra.Ring.Int.Parity
Int.instDecidablePredOdd : DecidablePred Odd
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.plusMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η : P ⟶ Q),
  J.plusMap η =
    { app := fun X => CategoryTheory.Limits.colimMap (J.diagramNatTrans η (Opposite.unop X)), naturality := ⋯ }
-- Mathlib.Topology.Compactness.Lindelof
IsClosed.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [LindelofSpace X], IsClosed s → IsLindelof s
-- Lean.PrettyPrinter.Basic
Lean.PrettyPrinter.backtrackExceptionId : Lean.InternalExceptionId
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxiHasSize : Std.Rxi.HasSize Int16
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonReferenceParams.toJson : Lean.Lsp.ReferenceParams → Lean.Json
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Given two morphisms of sheaves of `R`-modules `f : free ι ⟶ free σ` and `g : free σ ⟶ M`
satisfying `H : f ≫ g = 0` and `IsColimit (CokernelCofork.ofπ g H)`, we obtain a
`Presentation M`.  -/
SheafOfModules.presentationOfIsCokernelFree : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {ι σ : Type u} →
              {M : SheafOfModules R} →
                (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) →
                  (g : SheafOfModules.free σ ⟶ M) →
                    (H : CategoryTheory.CategoryStruct.comp f g = 0) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H) → M.Presentation
-- Mathlib.CategoryTheory.Join.Sum
/-- Characterization of `fromSum` with respect to the left inclusion.  -/
CategoryTheory.Join.inlCompFromSum : (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] →
        (CategoryTheory.Sum.inl_ C D).comp (CategoryTheory.Join.fromSum C D) ≅ CategoryTheory.Join.inclLeft C D
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.module' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {S : Type u_3} →
            [inst_3 : Semiring S] →
              [inst_4 : SMul S R] →
                [inst_5 : Module S M] → [IsScalarTower S R M] → (P : Submodule R M) → Module S (M ⧸ P)
-- Init.GrindInstances.ToInt
Lean.Grind.instLTBitVecUint : ∀ {v : ℕ}, Lean.Grind.ToInt.LT (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Mathlib.Data.Fintype.Basic
/-- Auxiliary definition to show `exists_seq_of_forall_finset_exists`.  -/
seqOfForallFinsetExistsAux : {α : Type u_4} →
  [DecidableEq α] →
    (P : α → Prop) → (r : α → α → Prop) → (∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y) → ℕ → α
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.ext : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {φ₁ φ₂ : A →ₗc[R] B}, (∀ (x : A), φ₁ x = φ₂ x) → φ₁ = φ₂
-- Aesop.Tree.Data
Aesop.TreeSpec.mk.sizeOf_spec : ∀ (Goal Rapp MVarCluster : Type) (introGoal : Aesop.GoalData Rapp MVarCluster → Goal)
  (elimGoal : Goal → Aesop.GoalData Rapp MVarCluster) (introRapp : Aesop.RappData Goal MVarCluster → Rapp)
  (elimRapp : Rapp → Aesop.RappData Goal MVarCluster) (introMVarCluster : Aesop.MVarClusterData Goal Rapp → MVarCluster)
  (elimMVarCluster : MVarCluster → Aesop.MVarClusterData Goal Rapp),
  sizeOf
      { Goal := Goal, Rapp := Rapp, MVarCluster := MVarCluster, introGoal := introGoal, elimGoal := elimGoal,
        introRapp := introRapp, elimRapp := elimRapp, introMVarCluster := introMVarCluster,
        elimMVarCluster := elimMVarCluster } =
    1 + sizeOf Goal + sizeOf Rapp + sizeOf MVarCluster
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.upShadow_compls : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)},
  𝒜.compls.upShadow = 𝒜.shadow.compls
-- Mathlib.Data.Real.Basic
Real.ind_mk : ∀ {C : ℝ → Prop} (x : ℝ), (∀ (y : CauSeq ℚ abs), C (Real.mk y)) → C x
-- Mathlib.Combinatorics.Colex
/-- If `s ≤ t` in colex and `#s ≤ #t`, then `s \ {a} ≤ t \ {min t}` for any `a ∈ s`.  -/
Finset.Colex.erase_le_erase_min' : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Finset α} {a : α},
  toColex s ≤ toColex t → ∀ (hcard : s.card ≤ t.card) (ha : a ∈ s), toColex (s.erase a) ≤ toColex (t.erase (t.min' ⋯))
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.sinhHomeomorph_symm_apply : ⇑Real.sinhHomeomorph.symm = EquivLike.inv Real.sinhOrderIso
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.ordered_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a b = Ordering.lt) t.keys
-- Mathlib.Data.SubtypeNeLift
Function.subtypeNeLift_self : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : ι → Type u_2} (i₀ : ι) (f : (j : { i // i ≠ i₀ }) → M ↑j) (x : M i₀),
  Function.subtypeNeLift i₀ f x i₀ = x
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_eq_zero_iff_le : ∀ {a b : Ordinal.{u_4}}, a - b = 0 ↔ a ≤ b
-- Init.Data.SInt.Lemmas
ISize.ofNat_div : ∀ {a b : ℕ},
  a < 2 ^ (System.Platform.numBits - 1) →
    b < 2 ^ (System.Platform.numBits - 1) → ISize.ofNat (a / b) = ISize.ofNat a / ISize.ofNat b
-- Mathlib.Algebra.Group.Defs
RightCancelMonoid.toRightCancelSemigroup : {M : Type u} → [self : RightCancelMonoid M] → RightCancelSemigroup M
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.ite_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : Prop} [inst_1 : Decidable P] {X Y Z : C} (g g' : Z ⟶ Y)
  (f : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (if P then g else g') f =
    if P then CategoryTheory.CategoryStruct.comp g f else CategoryTheory.CategoryStruct.comp g' f
-- Lean.Meta.Tactic.Simp.Main
/-- Return true if `e` is of the form `ofScientific n b m` where `n` and `m` are kernel Nat literals.  -/
Lean.Meta.Simp.isOfScientificLit : Lean.Expr → Bool
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_self_const_mul' : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {c : R},
  IsUnit c → ∀ (f : α → R) (l : Filter α), f =O[l] fun x => c * f x
-- Init.Data.UInt.Lemmas
USize.ofNatTruncate_uInt8ToNat : ∀ (n : UInt8), USize.ofNatClamp n.toNat = n.toUSize
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csInf_iff' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} [WellFoundedLT α],
  s.Nonempty → (b ≤ sInf s ↔ b ∈ lowerBounds s)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.not_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v}, p.IsCycle → ¬p.Nil
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.entryAtIdxD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → ∀ {i : ℕ} {fallback : (a : α) × β a}, t₁.entryAtIdxD i fallback = t₂.entryAtIdxD i fallback
-- Lean.Server.Requests
Lean.Server.RequestError.mk : Lean.JsonRpc.ErrorCode → String → Lean.Server.RequestError
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.mk : {E : Type uE} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type uH} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type uM} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] →
                  {c : M} →
                    (toContDiffBump : ContDiffBump (↑(extChartAt I c) c)) →
                      Metric.closedBall (↑(extChartAt I c) c) toContDiffBump.rOut ∩ Set.range ↑I ⊆
                          (extChartAt I c).target →
                        SmoothBumpFunction I c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.union_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp}, t₁.union t₂ = t₁ ∪ t₂
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.whiskerEquiv_inv_eq_lift : ∀ {J : Type w} {K : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f] [inst_3 : CategoryTheory.Limits.HasBiproduct g],
  (CategoryTheory.Limits.biproduct.whiskerEquiv e w).inv =
    CategoryTheory.Limits.biproduct.lift fun j =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π g (e j)) (w j).hom
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- If `R` has field of fractions `ℚ` and is the integral closure of `ℤ` in `ℚ` then it is
isomorphic to `ℤ`.  -/
Rat.IsIntegralClosure.intEquiv : (R : Type u_1) → [inst : CommRing R] → [inst_1 : Algebra R ℚ] → [IsIntegralClosure R ℤ ℚ] → R ≃+* ℤ
-- Mathlib.Data.Finsupp.Order
Finsupp.mapDomain_nonneg : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  {f : ι → κ} {g : ι →₀ α}, 0 ≤ g → 0 ≤ Finsupp.mapDomain f g
-- Mathlib.Analysis.ODE.Gronwall
/-- If `f` and `g` are two approximate solutions of the same ODE, then the distance between them
can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some
people call this Grönwall's inequality too.

This version assumes all inequalities to be true in some time-dependent set `s t`,
and assumes that the solutions never leave this set.  -/
dist_le_of_approx_trajectories_ODE_of_mem : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g f' g' : ℝ → E} {a b εf εg δ : ℝ},
  (∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (f' t) (Set.Ici t) t) →
        (∀ t ∈ Set.Ico a b, dist (f' t) (v t (f t)) ≤ εf) →
          (∀ t ∈ Set.Ico a b, f t ∈ s t) →
            ContinuousOn g (Set.Icc a b) →
              (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (g' t) (Set.Ici t) t) →
                (∀ t ∈ Set.Ico a b, dist (g' t) (v t (g t)) ≤ εg) →
                  (∀ t ∈ Set.Ico a b, g t ∈ s t) →
                    dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ gronwallBound δ (↑K) (εf + εg) (t - a)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instUniformSpace : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                UniformSpace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.Logic.Encodable.Pi
/-- When `α` is finite and `β` is encodable, `α → β` is encodable too. Because the encoding is not
unique, we wrap it in `Trunc` to preserve computability.  -/
Encodable.fintypeArrow : (α : Type u_2) → (β : Type u_3) → [DecidableEq α] → [Fintype α] → [Encodable β] → Trunc (Encodable (α → β))