mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Evaluate coefficients of the `HahnSeries` given an arbitrary input that's not necessarily in
`f`'s domain. The coefficient is picked from `y` that is "close enough" to `x` (their difference
is in a higher `ArchimedeanClass`). If no such `y` exists (in other words, x is "isolated"), set the
coefficient to 0.

This doesn't immediately extend `f`'s domain to the entire module in a consistent way. Such
extension isn't necessarily linear.
 -/
HahnEmbedding.Partial.evalCoeff : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                HahnEmbedding.Partial seed → M → FiniteArchimedeanClass M → R
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonFilePath : Lean.ToJson System.FilePath
-- Mathlib.GroupTheory.Sylow
/-- If `H` is a `p`-subgroup but not a Sylow `p`-subgroup of cardinality `p ^ n`,
then `p ^ (n + 1)` divides the cardinality of the normalizer of `H`.  -/
Sylow.prime_pow_dvd_card_normalizer : ∀ {G : Type u} [inst : Group G] [Finite G] {p n : ℕ} [_hp : Fact (Nat.Prime p)],
  p ^ (n + 1) ∣ Nat.card G → ∀ {H : Subgroup G}, Nat.card ↥H = p ^ n → p ^ (n + 1) ∣ Nat.card ↥(Subgroup.normalizer ↑H)
-- Mathlib.Topology.Algebra.Module.Complement
/-- If two submodules are topological complements, then the linear equivalence
`Submodule.quotientEquivOfIsCompl` is a homeomorphism, bundled as a continuous linear
equivalence.  -/
Submodule.quotientEquivOfIsTopCompl : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] →
            (p q : Submodule R M) → [IsTopologicalAddGroup M] → Submodule.IsTopCompl p q → (M ⧸ p) ≃L[R] ↥q
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- a functor that interprets element of `D` as functors `C ⥤ V`  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι : (C : Type u₁) →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    (V : Type u₂) →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            (D : Type u₃) →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                {inst_5 : CategoryTheory.MonoidalCategoryStruct D} →
                  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    CategoryTheory.Functor D (CategoryTheory.Functor C V)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.monoid : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] →
      [inst_1 : AddMonoid M] →
        [inst_2 : DistribMulAction R M] →
          [inst_3 : DistribMulAction Rᵐᵒᵖ M] → [SMulCommClass R Rᵐᵒᵖ M] → Monoid (TrivSqZeroExt R M)
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasStrictFDerivAt.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt g g' x → HasStrictFDerivAt (f - g) (f' - g') x
-- Init.Data.Array.Count
List.count_toArray : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a : α}, Array.count a l.toArray = List.count a l
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHom_mapDomainOfBialgHom : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H),
  AddMonoidAlgebra.mapDomainBialgHom R (AddMonoidAlgebra.mapDomainOfBialgHom f) = f
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv`. -/
NumberField.toNNReal_valued_eq_adicAbv : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R]
  (x : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K v)),
  ↑((WithZeroMulInt.toNNReal ⋯) (Valued.v x)) =
    (NumberField.HeightOneSpectrum.adicAbv K v) ((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)) x)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.isLittleO : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u v → (u - v) =o[l] v
-- Mathlib.Algebra.Order.UpperLower
mul_upperClosure : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] (s t : Set α),
  s * ↑(upperClosure t) = ↑(upperClosure (s * t))
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdLocallyUniformly.tendstoLocallyUniformly_finsetRange : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] {g : β → α} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β] {f : ℕ → β → α},
  HasProdLocallyUniformly f g → TendstoLocallyUniformly (fun x1 x2 => ∏ i ∈ Finset.range x1, f i x2) g Filter.atTop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.replicate.sizeOf_spec : ∀ {w w' : ℕ} (n : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w) (h : w' = w * n),
  sizeOf (Std.Tactic.BVDecide.BVExpr.replicate n expr h) = 1 + sizeOf w + sizeOf w' + sizeOf n + sizeOf expr + sizeOf h
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- If `f` and `g` are Lipschitz functions, so is the induced map `f × g` to the product type.  -/
LipschitzWith.prodMk : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {f : α → β} {Kf : NNReal},
  LipschitzWith Kf f → ∀ {g : α → γ} {Kg : NNReal}, LipschitzWith Kg g → LipschitzWith (max Kf Kg) fun x => (f x, g x)
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- The canonical algebra isomorphism from an `R`-algebra `R'` with an absolute value `v`
to `R'`.  -/
WithAbs.algEquiv : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      (R : Type u_3) →
        {T : Type u_4} →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring T] → [inst_4 : Algebra R T] → (v : AbsoluteValue T S) → WithAbs v ≃ₐ[R] T
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.instIsNoetherianOfFinite : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite R M], IsNoetherian R M
-- Mathlib.Order.Max
isMin_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMin (OrderDual.ofDual a) ↔ IsMax a
-- Mathlib.Data.Quot
/-- If `ra` is a subrelation of `ra'`, then we have a natural map `Quot ra → Quot ra'`.  -/
Quot.mapRight : {α : Sort u_1} → {ra ra' : α → α → Prop} → (∀ (a₁ a₂ : α), ra a₁ a₂ → ra' a₁ a₂) → Quot ra → Quot ra'
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_insertMany_list : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, k ∈ m.insertMany l ↔ k ∈ m ∨ l.contains k = true
-- Mathlib.Tactic.Translate.Reorder
/-- Compute where `ArgReorder.permute!` sends the `n`-th element in an array.  -/
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.ArgReorder.reverse.permuteSingle : Mathlib.Tactic.Translate.ArgReorder → ℕ → ℕ
-- Aesop.BuiltinRules.Subst
Aesop.BuiltinRules.matchSubstitutableIff? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_modify_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k}, (m.modify k f).get? k = Option.map f (m.get? k)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_le_ceil : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a b : R}, a ≤ b → ⌈a⌉₊ ≤ ⌈b⌉₊
-- Mathlib.Data.List.Sigma
List.dlookup_isSome : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)},
  (List.dlookup a l).isSome = true ↔ a ∈ l.keys
-- Init.Data.String.Basic
String.Pos.cast_le_iff : ∀ {s t : String} {pos : s.Pos} {pos' : t.Pos} {h : s = t}, pos.cast h ≤ pos' ↔ pos ≤ pos'.cast ⋯
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.L1.integrable_coeFn : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : ↥(MeasureTheory.Lp β 1 μ)), MeasureTheory.Integrable (↑↑f) μ
-- Lean.Data.Lsp.Basic
Lean.Lsp.VersionedTextDocumentIdentifier.mk : Lean.Lsp.DocumentUri → Option ℕ → Lean.Lsp.VersionedTextDocumentIdentifier
-- Mathlib.Analysis.Complex.RiemannMapping
/-- Proof of the Riemann Mapping Theorem, step 2.

If `U` is an open simply connected subset of `ℂ` which is not the whole field,
then there exists a map `f : ℂ → ℂ` such that

- `f` maps `U` to the unit disk;
- `f` is injective on `U`;
- `f` is differentiable on `U` with nonzero derivative.

Once the proof of the Riemann Mapping Theorem gets merged into Mathlib,
this lemma will be made private.
 -/
_private.Mathlib.Analysis.Complex.RiemannMapping.0.Complex.exists_mapsTo_unitBall_injOn_deriv_ne_zero : ∀ {U : Set ℂ},
  IsOpen U →
    IsSimplyConnected U → U ≠ Set.univ → ∃ f, Set.MapsTo f U (Metric.ball 0 1) ∧ Set.InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0
-- Mathlib.Data.Finmap
/-- `sdiff s s'` consists of all key-value pairs from `s` and `s'` where the keys are in `s` or
`s'` but not both.  -/
Finmap.sdiff : {α : Type u} → {β : α → Type v} → [DecidableEq α] → Finmap β → Finmap β → Finmap β
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Mathlib.Order.Disjoint
disjoint_iff_inf_le : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b ≤ ⊥
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The top-left `u × l` part of a `(u+d) × (l+r)` matrix.  -/
Matrix.subUpLeft : {α : Type v} → {d u l r : ℕ} → Matrix (Fin (u + d)) (Fin (l + r)) α → Matrix (Fin u) (Fin l) α
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mem_toSubsemigroup : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : AddSubmonoid M} {x : M}, x ∈ s.toAddSubsemigroup ↔ x ∈ s
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a lattice inherits a complement.  -/
BooleanSubalgebra.instComplCoe : {α : Type u_2} → [inst : BooleanAlgebra α] → {L : BooleanSubalgebra α} → Compl ↥L
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- This instance can be found using `Functor.hasBiproduct_of_preserves'`, but it is faster
to keep it here.  -/
CategoryTheory.Mat_.instHasBiproductιObjEmbeddingXOfAdditive : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [F.Additive] (M : CategoryTheory.Mat_ C),
  CategoryTheory.Limits.HasBiproduct fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))
-- Mathlib.Data.Finset.Max
Finset.notMem_of_lt_min : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a b : α}, a < b → s.min = ↑b → a ∉ s
-- Mathlib.GroupTheory.Index
AddAction.index_stabilizer_of_transitive : ∀ (G : Type u_1) {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] (x : X) [AddAction.IsPretransitive G X],
  (AddAction.stabilizer G x).index = Nat.card X
-- Mathlib.Data.List.SplitBy
List.splitBy_of_isChain : ∀ {α : Type u_1} {r : α → α → Bool} {l : List α},
  l ≠ [] → List.IsChain (fun x y => r x y = true) l → List.splitBy r l = [l]
-- Mathlib.Logic.Relation
Equivalence.eqvGen_eq : ∀ {α : Type u_1} {r : α → α → Prop}, Equivalence r → Relation.EqvGen r = r
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.out_eq' : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) (q : DoubleCoset.Quotient ↑H ↑K),
  DoubleCoset.mk H K (Quotient.out q) = q
-- Mathlib.Algebra.Regular.Defs
/-- An add-regular element is an element `c` such that addition by `c` both on the left and
on the right is injective.  -/
IsAddRegular : {R : Type u_2} → [Add R] → R → Prop
-- Mathlib.Algebra.Group.Units.Defs
/-- The additive inverse value of `val` in the base `AddMonoid`.  -/
AddUnits.neg : {α : Type u} → [inst : AddMonoid α] → AddUnits α → α
-- Mathlib.Analysis.Meromorphic.NormalForm
MeromorphicAt.meromorphicOrderAt_nonneg_iff_analyticAt_toMeromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → (0 ≤ meromorphicOrderAt f x ↔ AnalyticAt 𝕜 (toMeromorphicNFAt f x) x)
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- A pointed Galois object is a Galois object with a fixed point of its fiber.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [CategoryTheory.GaloisCategory C] → CategoryTheory.Functor C FintypeCat → Type (max u₁ u₂ w)
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic)
to the multiplicative integers, or is densely ordered, exclusively.

(See also `LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered`.)  -/
LinearOrderedCommGroup.discrete_iff_not_denselyOrdered : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G],
  Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.toEquiv_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), ↑f.symm = (↑f).symm
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.ΓSpecIso_inv : ∀ (R : CommRingCat),
  (AlgebraicGeometry.Scheme.ΓSpecIso R).inv =
    CommRingCat.ofHom (algebraMap (↑R) ((AlgebraicGeometry.structureSheafInType ↑R ↑R).obj.obj (Opposite.op ⊤)))
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.instReflectiveLocallyRingedSpaceOppositeCommRingCatToLocallyRingedSpace : CategoryTheory.Reflective AlgebraicGeometry.Spec.toLocallyRingedSpace
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₃ : CategoryTheory.LocalizedMonoidal L W ε} (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) f₃)
      (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ f₃))
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
ExistsAddOfLE.mk : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α], (∀ {a b : α}, a ≤ b → ∃ c, b = a + c) → ExistsAddOfLE α
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftHomologyIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂) {Z : C}
  (h : S₂.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.leftHomologyIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ)
      (CategoryTheory.CategoryStruct.comp S₂.leftHomologyIso.inv h)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.post_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) {X Y : CategoryTheory.StructuredArrow S F} (f : X ⟶ Y),
  (CategoryTheory.StructuredArrow.post S F G).map f =
    CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right f) ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.unitOfList_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  Std.ExtDTreeMap.Const.unitOfList l cmp = ∅ ↔ l = []
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.toAddSubgroup_le : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p p' : Submodule R M),
  p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p'
-- Batteries.Data.UInt
UInt64.le_iff_toNat_le_toNat : ∀ {x y : UInt64}, x ≤ y ↔ x.toNat ≤ y.toNat
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.devosMulRel_of_le_of_le : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {x y : Finset α × Finset α},
  (x.1 * x.2).card ≤ (y.1 * y.2).card →
    y.1.card + y.2.card ≤ x.1.card + x.2.card → x.1.card < y.1.card → DevosMulRel✝ x y
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_add' : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a b : ℚ},
  ↑a.den ≠ 0 →
    ↑b.den ≠ 0 →
      Lean.Grind.Field.NormNum.ofRat (a + b) = Lean.Grind.Field.NormNum.ofRat a + Lean.Grind.Field.NormNum.ofRat b
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {toOrderHom : α →o β}
  {exists_map_eq_of_map_le' : ∀ ⦃a : α⦄ ⦃b : β⦄, toOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toOrderHom.toFun c = b}
  {toOrderHom_1 : α →o β}
  {exists_map_eq_of_map_le'_1 : ∀ ⦃a : α⦄ ⦃b : β⦄, toOrderHom_1.toFun a ≤ b → ∃ c, a ≤ c ∧ toOrderHom_1.toFun c = b},
  { toOrderHom := toOrderHom, exists_map_eq_of_map_le' := exists_map_eq_of_map_le' } =
      { toOrderHom := toOrderHom_1, exists_map_eq_of_map_le' := exists_map_eq_of_map_le'_1 } →
    toOrderHom = toOrderHom_1
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulForall : {M : Type u_1} → {β : Type u_2} → {α : Type u_3} → [SMul M α] → SMul Mᵈᵐᵃ (α → β)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_image : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {ι : Type u_5} {ι' : Type u_6} {s : Set ι} {f : ι → ι'}
  {g : ι' → α}, BddBelow (Set.range fun i => g (f ↑i)) → ⨅ i, g (f ↑i) ≤ sInf ∅ → ⨅ i ∈ f '' s, g i = ⨅ x ∈ s, g (f x)
-- Mathlib.Analysis.Complex.Schwarz
/-- Let `f : E → F` be a complex analytic map
sending an open ball of radius `R₁` to a closed ball of radius `R₂`.
If `f w - f c = o(‖w - c‖ ^ n)`, then for any `z` in the ball in the domain,
we have `dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)`.

For `n = 0`, this theorem gives a usual Schwarz lemma,
see `dist_le_div_mul_dist_of_mapsTo_ball` below.
 -/
Complex.dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {c z : E} {R₁ R₂ : ℝ} {n : ℕ},
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) →
      ((fun x => f x - f c) =o[nhds c] fun w => ‖w - c‖ ^ n) →
        z ∈ Metric.ball c R₁ → dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.IndexingMode.elab : Array Lean.Syntax → Aesop.ElabM Aesop.IndexingMode
-- Mathlib.Algebra.Torsor.Defs
vadd_vsub_eq_sub_vsub : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (g : G) (p q : P), (g +ᵥ p) -ᵥ q = g - (q -ᵥ p)
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.bddBelow_range_of_cofinite : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [IsCodirectedOrder β] {f : α → β},
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) Filter.cofinite f → BddBelow (Set.range f)
-- Init.Util
withPtrEqUnsafe : {α : Type u} → (a b : α) → (k : Unit → Bool) → (a = b → k () = true) → Bool
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Int.mem_zmultiples_iff : ∀ {a b : ℤ}, b ∈ AddSubgroup.zmultiples a ↔ a ∣ b
-- Mathlib.Probability.Martingale.Upcrossing
/-- The number of upcrossings (strictly) before time `N`.  -/
MeasureTheory.upcrossingsBefore : {Ω : Type u_1} → {ι : Type u_2} → [inst : Preorder ι] → [OrderBot ι] → [InfSet ι] → ℝ → ℝ → (ι → Ω → ℝ) → ι → Ω → ℕ
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryGT.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.gt) → Sort u_3)
  (size : ℕ) (ky : α) (y : β) (l r : Std.DTreeMap.Internal.Impl α fun x => β)
  (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_2 size ky y l r ho he
-- Mathlib.Computability.NFA
NFA.evalFrom_cons : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (a : α) (x : List α),
  M.evalFrom S (a :: x) = M.evalFrom (M.stepSet S a) x
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChange.congr_simp : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (M : Type u_10) [inst_12 : AddCommGroup M] [inst_13 : Module R M]
  [inst_14 : Module A M] [inst_15 : IsScalarTower R A M],
  Algebra.IsPushout.cancelBaseChange R S A B M = Algebra.IsPushout.cancelBaseChange R S A B M
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor D C) {Z : D}
  {T : CategoryTheory.Presieve (F.obj Z)} {x : CategoryTheory.Presieve.FamilyOfElements P T},
  x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.functorPullback F x).Compatible