mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.adjoin_toSubalgebra_of_isAlgebraic : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  (∀ x ∈ S, IsAlgebraic F x) → (IntermediateField.adjoin F S).toSubalgebra = Algebra.adjoin F S
-- Mathlib.Algebra.Homology.ComplexShape
/-- The "composition" of two `ComplexShape`s.

We need this to define "related in k steps" later.
 -/
ComplexShape.trans : {ι : Type u_1} → ComplexShape ι → ComplexShape ι → ComplexShape ι
-- Std.Data.ExtHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.ExtHashMap.getKeyD : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → α → α
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.hasFDerivAt_fourierChar_neg_bilinear_right : ∀ {V : Type u_1} {W : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : NormedAddCommGroup W]
  [inst_3 : NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (v : V) (w : W),
  HasFDerivAt (fun w => ↑(Real.fourierChar (-(L v) w)))
    ((-2 * ↑Real.pi * Complex.I * ↑(Real.fourierChar (-(L v) w))) • Complex.ofRealCLM ∘SL L v) w
-- Mathlib.Tactic.NormNum.Inv
/-- The `norm_num` extension which identifies expressions of the form `NNRat.divNat a b`,
such that `norm_num` successfully recognises both `a` and `b`, and returns `a / b`.  -/
Mathlib.Meta.NormNum.evalNNRatDivNat : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfCone_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.coconeRightOpOfCone c).pt = Opposite.op c.pt
-- Mathlib.Data.Multiset.Fintype
/-- As a convenience, there is a coercion from `m : Type*` to `α` by projecting onto the first
component.  -/
Multiset.instCoeSortMultisetType.instCoeOutToType : {α : Type u_1} → [inst : DecidableEq α] → {m : Multiset α} → CoeOut m.ToType α
-- Mathlib.Data.Option.Basic
Option.elim_comp₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β → γ) {f : γ → α} {x : α} {g : γ → β} {y : β} {i : Option γ},
  (i.elim (h x y) fun j => h (f j) (g j)) = h (i.elim x f) (i.elim y g)
-- Mathlib.Topology.PartitionOfUnity
/-- the functions sum up to at most one, globally  -/
PartitionOfUnity.sum_le_one' : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ}
  (self : PartitionOfUnity ι X s) (x : X), ∑ᶠ (i : ι), (self.toFun i) x ≤ 1
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.notMem_of_notMem_closure : ∀ {G : Type u_1} [inst : Group G] {k : Set G} {P : G}, P ∉ Subgroup.closure k → P ∉ k
-- Mathlib.Topology.Order.Basic
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(-∞, x)` is separated below from `f x` is countable. We give
here a version relative to a set `t`.  -/
countable_image_lt_image_Iio_within : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α),
  {x | x ∈ t ∧ ∃ z < f x, ∀ y ∈ t, y < x → f y ≤ z}.Countable
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.instIsAddCommutativeSubtypeMem : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [IsAddCommutative G], IsAddCommutative ↥H
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- This is a version of `mem_span_set` with an estimate on the number of terms in the sum.  -/
Submodule.mem_span_set_iff_exists_finsupp_le_finrank : ∀ {K : Type u_2} {M : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup M] [inst_2 : Module K M] {s : Set M}
  {x : M} [Module.Finite K ↥(Submodule.span K s)],
  x ∈ Submodule.span K s ↔
    ∃ c, c.support.card ≤ Module.finrank K ↥(Submodule.span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = x
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Graded ring homomorphisms preserve subtraction.  -/
GradedRingHom.map_sub : ∀ {ι : Type u_1} {A : Type u_10} {B : Type u_11} {σ : Type u_12} {τ : Type u_13} [inst : Ring A] [inst_1 : Ring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] (𝒜 : ι → σ) (ℬ : ι → τ) (f : 𝒜 →+*ᵍ ℬ) (x y : A), f (x - y) = f x - f y
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_erase : ∀ {M : Type u_4} [inst : AddCommMonoid M] {a : M} {l : List M} [inst_1 : DecidableEq M],
  a ∈ l → a + (l.erase a).sum = l.sum
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- `locallyConstantIsoContinuousMap` is a natural isomorphism.  -/
CompHausLike.LocallyConstant.functorToPresheavesIso : (P : TopCat → Prop) →
  [inst : CompHausLike.HasExplicitFiniteCoproducts P] →
    [inst_1 : CompHausLike.HasExplicitPullbacks P] →
      (hs :
          ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
            CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
        (X : Type (max u w)) →
          CompHausLike.LocallyConstant.functorToPresheaves.obj X ≅
            (TopCat.toSheafCompHausLike P (TopCat.discrete.obj X) hs).obj
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_map : ∀ {x y : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)} (h : x ⟶ y),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.functor.map h =
    match x, y, h with
    | x, .(x), CategoryTheory.Limits.WalkingParallelFamily.Hom.id .(x) =>
      CategoryTheory.CategoryStruct.id
        (CategoryTheory.Limits.WalkingParallelFamily.rec CategoryTheory.Limits.WalkingParallelPair.zero
          CategoryTheory.Limits.WalkingParallelPair.one x)
    | .(CategoryTheory.Limits.WalkingParallelFamily.zero), .(CategoryTheory.Limits.WalkingParallelFamily.one),
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line j =>
      bif j.down then CategoryTheory.Limits.WalkingParallelPairHom.left
      else CategoryTheory.Limits.WalkingParallelPairHom.right
-- Mathlib.GroupTheory.PushoutI
/-- The data we need to pick a normal form for words in the pushout. We need to pick a
canonical element of each coset. We also need all the maps in the diagram to be injective  -/
Monoid.PushoutI.NormalWord.Transversal : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} → [inst : (i : ι) → Group (G i)] → [inst_1 : Group H] → ((i : ι) → H →* G i) → Type (max u_1 u_2)
-- Mathlib.RingTheory.Ideal.Maps
element_smul_restrictScalars : ∀ {R : Type u_4} {S : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (r : R)
  (N : Submodule S M), Submodule.restrictScalars R ((algebraMap R S) r • N) = r • Submodule.restrictScalars R N
-- Mathlib.Data.ZMod.QuotientGroup
infinite_zpowers : ∀ {α : Type u_3} [inst : Group α] {a : α}, (↑(Subgroup.zpowers a)).Infinite ↔ ¬IsOfFinOrder a
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instAddCommGroup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] → [inst_1 : SeminormedAddCommGroup β] → AddCommGroup (BoundedContinuousFunction α β)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_preAleph : ∀ (o : Ordinal.{u}), Cardinal.lift.{v, u} (Cardinal.preAleph o) = Cardinal.preAleph (Ordinal.lift.{v, u} o)
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.natIsoFunctor_inv_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁}
  {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (X : CategoryTheory.Discrete I),
  CategoryTheory.Discrete.natIsoFunctor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.CategoryTheory.MorphismProperty.Ind
/-- A property of morphisms `P` is said to pre-ind-spread if `P`-morphisms out of filtered colimits
descend to a finite level. More precisely, let `Dᵢ` be a filtered family of objects.
Then:

- If `f : colim Dᵢ ⟶ T` satisfies `P`, there exists an index `j` and a pushout square
  ```
    Dⱼ ----f'---> T'
    |             |
    |             |
    v             v
  colim Dᵢ --f--> T
  ```
  such that `f'` satisfies `P`.
 -/
CategoryTheory.MorphismProperty.PreIndSpreads : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Init.Data.Iterators.Consumers.Collect
/-- Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toList`.
 -/
Std.Iter.Total.toList : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.Iterators.Finite α Id] → Std.Iter.Total β → List β
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ : MeasureTheory.ProbabilityMeasure Ω) (f : BoundedContinuousFunction Ω NNReal),
  μ.toWeakDualBCNN f = (∫⁻ (ω : Ω), ↑(f ω) ∂↑μ).toNNReal
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ι_tensorObjDesc : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ : CategoryTheory.GradedObject I C} [inst_3 : X₁.HasTensor X₂]
  {A : C} {k : I}
  (f : (i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)) (i₁ i₂ : I)
  (hi : i₁ + i₂ = k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ k hi)
      (CategoryTheory.GradedObject.Monoidal.tensorObjDesc f) =
    f i₁ i₂ hi
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.ceil_map_map_zero_le : ∀ (f g : CircleDeg1Lift), ⌈f (g 0)⌉ ≤ ⌈f 0⌉ + ⌈g 0⌉
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isPrestackFor_iff_isSheafFor' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  (R : CategoryTheory.Sieve S),
  F.IsPrestackFor R.arrows ↔
    ∀ ⦃S₀ : C⦄ (M N : ↑(F.obj { as := Opposite.op S₀ })) (a : S ⟶ S₀),
      CategoryTheory.Presieve.IsSheafFor (F.presheafHom M N)
        ((CategoryTheory.Sieve.overEquiv (CategoryTheory.Over.mk a)).symm R).arrows
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.TheoremForm.uncurried : Mathlib.Meta.FunProp.TheoremForm
-- Mathlib.Order.PFilter
/-- There is a bottom filter when `P` has a top element.  -/
Order.PFilter.instOrderBot : {P : Type u_1} → [inst : Preorder P] → [OrderTop P] → OrderBot (Order.PFilter P)
-- Mathlib.GroupTheory.FiniteAbelian.Basic
_private.Mathlib.GroupTheory.FiniteAbelian.Basic.0.directSumNeZeroMulHom : {ι : Type} →
  [DecidableEq ι] →
    (p n : ι → ℕ) → (DirectSum { i // n i ≠ 0 } fun i => ZMod (p ↑i ^ n ↑i)) →+ DirectSum ι fun i => ZMod (p i ^ n i)
-- Lean.Parser.Module
Lean.Parser.isTerminalCommand : Lean.Syntax → Bool
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le' : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (X : CategoryTheory.Abelian.SpectralObject C ι)
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) [X.HasSpectralSequence data] (r r' : ℤ)
  (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq : κ),
  (∀ (pq' : κ), ¬(c r).Rel pq' pq) →
    ∀ (n : ℤ),
      n = data.deg pq - 1 →
        ∀ (i₃ i₃' : ι) (hi₃ : i₃ = data.i₃ r pq ⋯) (hi₃' : i₃' = data.i₃ r' pq ⋯),
          CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k a : α} [inst_1 : Inhabited (β a)] {v : β k},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.get! a = if h : compare k a = Ordering.eq then cast ⋯ v else t.get! a
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.path_apply : ∀ (x y : Circle) (a : ↑unitInterval), (x.path y) a = Circle.exp ((Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) a)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), Measurable ⇑e
-- Init.Data.Sum.Basic
/-- Checks whether a sum is the left injection `inl` and, if so, retrieves its contents.  -/
Sum.getLeft? : {α : Type u_1} → {β : Type u_2} → α ⊕ β → Option α
-- Qq.Macro
/-- Quoted mvars in the outside lctx (of type `Level`, `Quoted _`, or `Type`).
The outside mvars can also be of the form `?m x y z`.
 -/
Qq.Impl.UnquoteState.mvars : Qq.Impl.UnquoteState → List (Lean.Expr × Qq.Impl.MVarSynth)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {he : t.isEmpty = false}, t.getKey! (t.maxKey he) = t.maxKey he
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.mk.injEq : ∀ {α : Type u_5} (toField : Field α) (toConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder α)
  [toIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid α] [toZeroLEOneClass : ZeroLEOneClass α]
  [toPosMulStrictMono : PosMulStrictMono α] [toMulPosStrictMono : MulPosStrictMono α] (toField_1 : Field α)
  (toConditionallyCompleteLinearOrder_1 : ConditionallyCompleteLinearOrder α)
  (toIsOrderedCancelAddMonoid_1 : IsOrderedCancelAddMonoid α) (toZeroLEOneClass_1 : ZeroLEOneClass α)
  (toPosMulStrictMono_1 : PosMulStrictMono α) (toMulPosStrictMono_1 : MulPosStrictMono α),
  ({ toField := toField, toConditionallyCompleteLinearOrder := toConditionallyCompleteLinearOrder,
        toIsOrderedCancelAddMonoid := toIsOrderedCancelAddMonoid, toZeroLEOneClass := toZeroLEOneClass,
        toPosMulStrictMono := toPosMulStrictMono, toMulPosStrictMono := toMulPosStrictMono } =
      { toField := toField_1, toConditionallyCompleteLinearOrder := toConditionallyCompleteLinearOrder_1,
        toIsOrderedCancelAddMonoid := toIsOrderedCancelAddMonoid_1, toZeroLEOneClass := toZeroLEOneClass_1,
        toPosMulStrictMono := toPosMulStrictMono_1, toMulPosStrictMono := toMulPosStrictMono_1 }) =
    (toField = toField_1 ∧ toConditionallyCompleteLinearOrder = toConditionallyCompleteLinearOrder_1)
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `F` reflects isomorphisms, then `functoriality F` reflects isomorphisms
as well.
 -/
CategoryTheory.Limits.Cone.reflects_cone_isomorphism : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms]
  (K : CategoryTheory.Functor J C), (CategoryTheory.Limits.Cone.functoriality K F).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.evaluation_preservesColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  [∀ (k : K), CategoryTheory.Limits.HasColimit (F.flip.obj k)] (k : K),
  CategoryTheory.Limits.PreservesColimit F ((CategoryTheory.evaluation K C).obj k)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symmEquiv_symm_apply_apply : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M₂ ≃ₛₗ[σ'] M) (a : M),
  (LinearEquiv.symmEquiv.symm e) a = ((↑e).inverse ⇑e.symm ⋯ ⋯) a
-- Mathlib.Order.Antichain
/-- **Alias** of `Std.Symm.compl`. -/
Symmetric.compl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm rᶜ
-- Mathlib.Data.Multiset.Bind
/-- The multiplicity of `(a, b)` in `s ×ˢ t` is
the product of the multiplicity of `a` in `s` and `b` in `t`.  -/
Multiset.product : {α : Type u_1} → {β : Type v} → Multiset α → Multiset β → Multiset (α × β)
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The number of rows in `ofRowLens w hw` is the length of `w`  -/
YoungDiagram.rowLens_length_ofRowLens : ∀ {w : List ℕ} {hw : w.SortedGE}, (∀ x ∈ w, 0 < x) → (YoungDiagram.ofRowLens w hw).rowLens.length = w.length
-- Std.Internal.UV.System
Std.Internal.UV.System.PasswdInfo.uid : Std.Internal.UV.System.PasswdInfo → Option UInt64
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHom_injective : ∀ {σ : Type u_1} (R : Type u_3) {n : ℕ} [inst : Fintype σ] [inst_1 : CommRing R],
  n ≤ Fintype.card σ → Function.Injective ⇑(MvPolynomial.esymmAlgHom σ R n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_maxKey!_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, t.contains k = true → (cmp k t.maxKey!).isLE = true
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.hasFiniteIntegral_prodMk_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] (a : α) {s : Set (β × γ)},
  ((κ.compProd η) a) s ≠ ⊤ → MeasureTheory.HasFiniteIntegral (fun b => (η (a, b)).real (Prod.mk b ⁻¹' s)) (κ a)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.mk : ∀ {α : Type u_3} {D : Set (Set α)} [inst : Preorder α] [inst_1 : TopologicalSpace α],
  inst_1 = Topology.scottHausdorff α D → Topology.IsScottHausdorff α D
-- Mathlib.Combinatorics.Graph.Basic
Graph.adj_comm : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} (x y : α), G.Adj x y ↔ G.Adj y x
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_vsub_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β}, (f -ᵥ g).NeBot → g.NeBot
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.extern : {pu : Lean.Compiler.LCNF.Purity} → Lean.ExternAttrData → Lean.Compiler.LCNF.DeclValue pu
-- Mathlib.Analysis.Analytic.Order
/-- The analytic order of the function `(· - c)` at `x` is one if `x = c`.  -/
analyticOrderAt_id_sub_const_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {c : 𝕜}, analyticOrderAt (fun x => x - c) c = 1
-- Lean.Meta.SynthInstance
/-- Return globals and locals instances that may unify with `type`  -/
Lean.Meta.SynthInstance.getInstances : Lean.Expr → Lean.MetaM (Array Lean.Meta.SynthInstance.Instance)
-- Mathlib.Analysis.Analytic.OfScalars
/-- Formal power series of `∑ cᵢ • xⁱ` for some scalar field `𝕜` and ring algebra `E`  -/
FormalMultilinearSeries.ofScalars : {𝕜 : Type u_1} →
  (E : Type u_2) →
    [inst : Field 𝕜] →
      [inst_1 : Ring E] →
        [inst_2 : Algebra 𝕜 E] →
          [inst_3 : TopologicalSpace E] → [inst_4 : IsTopologicalRing E] → (ℕ → 𝕜) → FormalMultilinearSeries 𝕜 E E
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.Indep.symm : ∀ {Ω : Type u_1} {m₁ m₂ _mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.Indep m₁ m₂ μ → ProbabilityTheory.Indep m₂ m₁ μ
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x ∂μ`.  -/
MeasureTheory.tendsto_integral_of_L1 : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : α → G),
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {F : ι → α → G} {l : Filter ι},
      (∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) →
        Filter.Tendsto (fun i => ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (nhds 0) →
          Filter.Tendsto (fun i => ∫ (x : α), F i x ∂μ) l (nhds (∫ (x : α), f x ∂μ))
-- Mathlib.Data.Complex.Basic
Complex.natCast_re : ∀ (n : ℕ), (↑n).re = ↑n
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.LiesOver.isometry_algebraMap : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [w.LiesOver v],
  Isometry ⇑(algebraMap (WithAbs ↑v) (WithAbs ↑w))
-- Mathlib.Data.Matrix.Basic
AlgEquiv.mapMatrix_apply : ∀ {m : Type u_2} {R : Type u_7} {α : Type u_11} {β : Type u_12} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : CommSemiring R] [inst_3 : Semiring α] [inst_4 : Semiring β] [inst_5 : Algebra R α] [inst_6 : Algebra R β]
  (f : α ≃ₐ[R] β) (M : Matrix m m α), f.mapMatrix M = M.map ⇑f
-- Init.Data.ByteArray.Basic
/-- Replaces the byte at the given index.

No bounds check is performed, but the function requires a proof that the index is in bounds. This
proof can usually be omitted, and will be synthesized automatically.

The array is modified in-place if there are no other references to it.
 -/
ByteArray.uset : (a : ByteArray) → (i : USize) → UInt8 → autoParam (i.toNat < a.size) ByteArray.uset._auto_1 → ByteArray
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.monomial_coe_mem_degreeLT : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} (i : Fin n) (a : R), (Polynomial.monomial ↑i) a ∈ Polynomial.degreeLT R n
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.corec_roll : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {X Y : Type u} {x₀ : X} (f : X → Y)
  (g : Y → F (α ::: X)), MvQPF.Cofix.corec (g ∘ f) x₀ = MvQPF.Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x₀)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W},
  G.IsContained H → G.vertexCoverNum ≤ H.vertexCoverNum
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
/-- This is the map `⨁ₘ G ⟶ A` induced by `M ⟶ Hom(G, A)`.  -/
CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] →
        {G A : C} →
          {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ} →
            (M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)) → ((∐ fun x => G) ⟶ A)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.mk.sizeOf_spec : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} [inst_3 : SizeOf A] [inst_4 : SizeOf B] [inst_5 : SizeOf T]
  [inst_6 : ⦃X Y : T⦄ → (x : X ⟶ Y) → SizeOf (P x)] [inst_7 : ⦃X Y : A⦄ → (x : X ⟶ Y) → SizeOf (Q x)]
  [inst_8 : ⦃X Y : B⦄ → (x : X ⟶ Y) → SizeOf (W x)] (toCommaMorphism : CategoryTheory.CommaMorphism X.toComma Y.toComma)
  (prop_hom_left : Q toCommaMorphism.left) (prop_hom_right : W toCommaMorphism.right),
  sizeOf { toCommaMorphism := toCommaMorphism, prop_hom_left := prop_hom_left, prop_hom_right := prop_hom_right } =
    1 + sizeOf toCommaMorphism + sizeOf prop_hom_left + sizeOf prop_hom_right