mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.getEntryGTD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Sigma β → (a : α) × β a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- `CategoricalPullback.π₂ F G` is the second projection `CategoricalPullback F G ⥤ C`.  -/
CategoryTheory.Limits.CategoricalPullback.π₂ : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                CategoryTheory.Functor (CategoryTheory.Limits.CategoricalPullback F G) C
-- Mathlib.Logic.Relation
Relation.reflTransGen_closed : ∀ {α : Type u_1} {r p : α → α → Prop}, r ≤ Relation.ReflTransGen p → Relation.ReflTransGen r ≤ Relation.ReflTransGen p
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_two : Nat.primesBelow 2 = ∅
-- Mathlib.Tactic.Contrapose
Mathlib.Tactic.Contrapose.contrapose₁ : ∀ {p q : Prop}, (¬q → ¬p) → p → q
-- Mathlib.Data.Set.Pairwise.Basic
Pairwise.disjoint_extend_bot : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PartialOrder γ] [inst_1 : OrderBot γ] {e : α → β} {f : α → γ},
  Pairwise (Function.onFun Disjoint f) →
    Function.FactorsThrough f e → Pairwise (Function.onFun Disjoint (Function.extend e f ⊥))
-- Init.Data.SInt.Lemmas
Int32.toInt32_toInt64 : ∀ (n : Int32), n.toInt64.toInt32 = n
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.coe_support_eq_set_support : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α), ↑f.support = {x | f x ≠ x}
-- Mathlib.Order.Hom.WithTopBot
SupHom.withBot_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β]
  [inst_2 : SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β), (f.comp g).withBot = f.withBot.comp g.withBot
-- Mathlib.Computability.Primrec.Basic
Primrec.of_equiv : ∀ {α : Type u_1} [inst : Primcodable α] {β : Type u_4} {e : β ≃ α}, Primrec ⇑e
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.vadd_def : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] (a : M) (x : (i : ι) × α i),
  a +ᵥ x = Sigma.map id (fun x x_1 => a +ᵥ x_1) x
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.nnqsmul_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : ℚ≥0) (m : M) (s : ℕ+),
  a • DivisibleHull.mk m s = DivisibleHull.mk (a.num • m) (⟨a.den, ⋯⟩ * s)
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.IterM.length : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → [Monad m] → Std.IterM m β → m (ULift.{w, 0} ℕ)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.smul_mem_pointwise_smul : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α M] (m : M) (a : α)
  (S : Submonoid M), m ∈ S → a • m ∈ a • S
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- If `p` is a prime and `IsCyclotomicExtension {p ^ k} K L`, then there are `u : ℤˣ` and
`n : ℕ` such that the discriminant of the power basis given by `ζ - 1` is `u * p ^ n`. Often this is
enough and less cumbersome to use than `IsCyclotomicExtension.Rat.discr_prime_pow'`.  -/
IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow' : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  ∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {toPrecoverage : CategoryTheory.Precoverage C}
  {pullback :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X), ∀ S ∈ toPrecoverage.coverings X, ∃ T ∈ toPrecoverage.coverings Y, T.FactorsThruAlong S f}
  {toPrecoverage_1 : CategoryTheory.Precoverage C}
  {pullback_1 :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
      ∀ S ∈ toPrecoverage_1.coverings X, ∃ T ∈ toPrecoverage_1.coverings Y, T.FactorsThruAlong S f},
  { toPrecoverage := toPrecoverage, pullback := pullback } =
      { toPrecoverage := toPrecoverage_1, pullback := pullback_1 } →
    toPrecoverage = toPrecoverage_1
-- Mathlib.Order.Filter.Extr
IsMaxOn.min : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {s : Set α},
  IsMaxOn f s a → IsMaxOn g s a → IsMaxOn (fun x => min (f x) (g x)) s a
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.prod_sum : ∀ {M : Type u_4} {ι : Type u_5} [inst : CommMonoid M] (f : ι → Multiset M) (s : Finset ι),
  (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod
-- Mathlib.Algebra.Module.LinearMap.Defs
IsLinearMap.mk'_apply : ∀ {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂} (lin : IsLinearMap R f) (x : M),
  (IsLinearMap.mk' f lin) x = f x
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.curry.eq_1 : ∀ (c : Nat.Partrec.Code) (n : ℕ), c.curry n = c.comp ((Nat.Partrec.Code.const n).pair Nat.Partrec.Code.id)
-- Lean.Util.MonadCache
Lean.MonadCache.cache : {α β : Type} → {m : Type → Type} → [self : Lean.MonadCache α β m] → α → β → m Unit
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.pure : Lean.TSyntax `term → Lean.Parser.Tactic.MRefinePat
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.sum_one_div_prime_eq_indicator_div_add : ∀ {k p : ℕ},
  k > 0 →
    ∀ [Fact (Nat.Prime p)],
      ∑ q ∈ Bernoulli.vonStaudtPrimes✝ k, 1 / ↑q =
        Bernoulli.vonStaudtIndicator✝ (2 * k) p / ↑p + ∑ q ∈ Bernoulli.vonStaudtPrimes✝ k with q ≠ p, 1 / ↑q
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_symm_apply : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] (F : AddMonoidAlgebra R M →ₐ[R] A) (x : Multiplicative M),
  ((AddMonoidAlgebra.lift R A M).symm F) x = F (AddMonoidAlgebra.single (Multiplicative.toAdd x) 1)
-- Init.Data.UInt.Lemmas
USize.pow_zero : ∀ (x : USize), x ^ 0 = 1
-- Mathlib.Data.List.Permutation
List.permutationsAux_append : ∀ {α : Type u_1} (is is' ts : List α),
  (is ++ ts).permutationsAux is' =
    List.map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
-- Plausible.Testable
/-- Run a test suite for `p` in `IO` using the global RNG in `stdGenRef`.  -/
Plausible.Testable.checkIO : (p : Prop) → [Plausible.Testable p] → optParam Plausible.Configuration { } → IO (Plausible.TestResult p)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) h
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.sUnion : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)},
  s.Countable → (∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ) → MeasureTheory.NullMeasurableSet (⋃₀ s) μ
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.charPoly_monic : ∀ {R : Type u_1} [inst : CommRing R] (E : LinearRecurrence R), E.charPoly.Monic
-- Lean.Elab.Tactic.Omega.MinNatAbs
/-- The minimum absolute value of a nonzero entry, or zero if all entries are zero.

We completely characterize the function via
`minNatAbs_eq_zero_iff` and `minNatAbs_eq_nonzero_iff` below.
 -/
Lean.Elab.Tactic.Omega.List.minNatAbs : List ℤ → ℕ
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.doubleDualEmb_bijective : ∀ {α : Type u_1} [inst : AddCommGroup α] [Finite α], Function.Bijective ⇑AddChar.doubleDualEmb
-- Mathlib.GroupTheory.Index
Subgroup.finite_quotient_of_pretransitive_of_index_ne_zero : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {X : Type u_3} [inst_1 : MulAction G X]
  [MulAction.IsPretransitive G X], H.index ≠ 0 → Finite (MulAction.orbitRel.Quotient (↥H) X)
-- Init.Control.Lawful.Instances
instLawfulFunctorExcept : ∀ {ε : Type u_1}, LawfulFunctor (Except ε)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_add_two : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.S R (n + 2) = Polynomial.X * Polynomial.Chebyshev.S R (n + 1) - Polynomial.Chebyshev.S R n
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_of_le_of_lt : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [inst_4 : Zero β] [PosSMulStrictMono α β] [SMulPosMono α β],
  a₁ ≤ a₂ → b₁ < b₂ → 0 < a₁ → 0 ≤ b₂ → a₁ • b₁ < a₂ • b₂
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opFunctor_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C)
  {n m : SimplexCategoryᵒᵖ} (f : n ⟶ m),
  (SimplicialObject.opFunctor.obj X).map f =
    CategoryTheory.CategoryStruct.comp SimplicialObject.opObjIso.hom
      (CategoryTheory.CategoryStruct.comp (X.map (SimplexCategory.rev.map f.unop).op) SimplicialObject.opObjIso.inv)
-- Mathlib.Topology.Compactness.CountablyCompact
/-- **Alias** of `LindelofSpace.compactSpace`.

---

A countably compact Lindelöf space is compact.  -/
LindelofSpace.CompactSpace : ∀ {X : Type u_4} [inst : TopologicalSpace X] [LindelofSpace X] [h : CountablyCompactSpace X], CompactSpace X
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.fill.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (t : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a)
  (h_3 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b),
  (match RBTree.RBNode.Path.root, t with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left c parent y b, a => h_2 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b => h_3 c a y parent b) =
    h_1 t
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.parser.inj : ∀ {catName declName : Lean.Name} {prio : ℕ} {catName_1 declName_1 : Lean.Name} {prio_1 : ℕ},
  Lean.Parser.ParserExtension.OLeanEntry.parser catName declName prio =
      Lean.Parser.ParserExtension.OLeanEntry.parser catName_1 declName_1 prio_1 →
    catName = catName_1 ∧ declName = declName_1 ∧ prio = prio_1
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.saturate_iff_saturate_toPrecoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C) {X : C}
  {S : CategoryTheory.Sieve X}, K.Saturate X S ↔ K.Saturate X S
-- Mathlib.RingTheory.LocalRing.Module
IsLocalRing.span_eq_top_of_tmul_eq_basis : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Module.Finite R M] {ι : Type u_5} (f : ι → M)
  (b : Module.Basis ι (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) M)),
  (∀ (i : ι), 1 ⊗ₜ[R] f i = b i) → Submodule.span R (Set.range f) = ⊤
-- Mathlib.Order.DirectedInverseSystem
DirectedSystem.map_self : ∀ {ι : Type u_1} {inst : Preorder ι} {F : ι → Type u_4} {f : ⦃i j : ι⦄ → i ≤ j → F i → F j} [self : DirectedSystem F f]
  ⦃i : ι⦄ (x : F i), f ⋯ x = x
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
/-- `(X.normalizedChainComplex R).X n` identifies to the coproduct of copies
of `R` indexed by the nondegenerate `n`-simplices of the simplicial set `X`.  -/
SSet.isColimitCofanNormalizedChainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) → (R : C) → (n : ℕ) → CategoryTheory.Limits.IsColimit (X.cofanNormalizedChainComplex R n)
-- Mathlib.GroupTheory.GroupExtension.Basic
SemidirectProduct.right_splitting : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N}
  (s : (SemidirectProduct.toGroupExtension φ).Splitting) (g : G), (s g).right = g
-- Mathlib.Data.Matrix.Basic
AddSubgroup.coe_matrix : ∀ {m : Type u_2} {n : Type u_3} {A : Type u_14} [inst : AddGroup A] (S : AddSubgroup A), ↑S.matrix = (↑S).matrix
-- Mathlib.RingTheory.Unramified.Basic
/-- If `S` is an unramified `R`-algebra, `S ⊗[R] S` splits as `S × T` for some `R`-algebra `T`.
In particular, the diagonal is an open and closed immersion.  -/
Algebra.FormallyUnramified.exists_algEquiv_prod : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.EssFiniteType R S]
  [Algebra.FormallyUnramified R S], ∃ T x x_1, Nonempty (TensorProduct R S S ≃ₐ[S] S × T)
-- Mathlib.Order.Filter.TendstoCofinite
Filter.TendstoCofinite.finite_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [Filter.TendstoCofinite f] (b : β), (f ⁻¹' {b}).Finite
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- If `u` is a monotone function with linear ordered codomain and the range of `u` is not bounded
below, then `Tendsto u atBot atBot`.  -/
Filter.tendsto_atBot_atBot_of_monotone' : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : LinearOrder α] {u : ι → α},
  Monotone u → ¬BddBelow (Set.range u) → Filter.Tendsto u Filter.atBot Filter.atBot
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_none : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∉ m → m.getKey? a = none
-- Batteries.Classes.Order
Std.instTransCmpCompareOnOfTransOrd_batteries : ∀ {β : Type u_1} {α : Type u_2} [inst : Ord β] [Std.TransOrd β] (f : α → β), Std.TransCmp (compareOn f)
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
/-- If `S` is a short exact short complex in a balanced category,
then `S.X₁` is the kernel of `S.g`.  -/
CategoryTheory.ShortComplex.ShortExact.fIsKernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Balanced C] →
        {S : CategoryTheory.ShortComplex C} →
          S.ShortExact → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)
-- Mathlib.RingTheory.Etale.Locus
Algebra.etaleLocus_eq_unramfiedLocus_inter_smoothLocus : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.etaleLocus R A = Algebra.unramifiedLocus R A ∩ Algebra.smoothLocus R A
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α)
  (f : α → MeasureTheory.Measure β), m.bind f = (MeasureTheory.Measure.map f m).join
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.getVert_tail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v), p.tail.getVert n = p.getVert (n + 1)
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `Equiv.mulLeft` as an `OrderIso`. See also `OrderEmbedding.mulLeft`.  -/
OrderIso.mulLeft : {α : Type u} → [inst : Group α] → [inst_1 : LE α] → [MulLeftMono α] → α → α ≃o α
-- Mathlib.Probability.ProductMeasure
/-- To prove that a measure is equal to the product measure it is enough to check that it
it gives the same measure to measurable boxes.  -/
MeasureTheory.Measure.eq_infinitePi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {ν : MeasureTheory.Measure ((i : ι) → X i)},
  (∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
      (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)) →
    ν = MeasureTheory.Measure.infinitePi μ
-- Lean.Meta.ArgsPacker
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Unary.pack.go : Array Lean.Expr → ℕ → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Galois.Topology
/-- For a functor `F : C ⥤ FintypeCat`, the canonical embedding of `Aut F` into
the product over `Aut (F.obj X)` for all objects `X`.  -/
CategoryTheory.PreGaloisCategory.autEmbedding : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → CategoryTheory.Aut F →* (X : C) → CategoryTheory.Aut (F.obj X)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq_zero_iff_of_nonneg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ f → MeasureTheory.Integrable f μ → (∫ (x : α), f x ∂μ = 0 ↔ f =ᵐ[μ] 0)
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
IsValuativeTopology.continuous_valuation : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R],
  Continuous ⇑(ValuativeRel.valuation R)
-- Mathlib.Algebra.Polynomial.SumIteratedDerivative
Polynomial.sumIDeriv_C : ∀ {R : Type u_1} [inst : Semiring R] (a : R), Polynomial.sumIDeriv (Polynomial.C a) = Polynomial.C a
-- Lean.Parser.Extra
Lean.ppDedent.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.fst_opProdIsoCoprod_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op (CategoryTheory.Limits.opProdIsoCoprod A B).hom =
    CategoryTheory.Limits.coprod.inl
-- Lean.Parser.Basic
Lean.Parser.nonReservedSymbolNoAntiquot : String → optParam Bool false → Lean.Parser.Parser
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.instDecidableLtOrigin : (a b : Lean.Meta.Origin) → Decidable (a < b)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.tail_val' : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} (B : Fin m.succ → n' → α) (j : n'),
  (Matrix.vecTail fun i => B i j) = fun i => Matrix.vecTail B i j
-- Init.Data.Nat.Basic
Nat.add_one_le_of_lt : ∀ {n m : ℕ}, n < m → n + 1 ≤ m
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_neg : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {x, -y} = Ideal.span {x, y}
-- Mathlib.Order.Hom.WithTopBot
/-- Taking the dual then adding `⊥` is the same as adding `⊤` then taking the dual.
This is the order iso form of `WithBot.ofDual`, as proven by `coe_toDualTopEquiv`.  -/
WithBot.toDualTopEquiv : {α : Type u_1} → [inst : LE α] → WithBot αᵒᵈ ≃o (WithTop α)ᵒᵈ
-- Lean.Data.Lsp.Internal
/-- Response for the `$/lean/queryModule` watchdog <- worker request.  -/
Lean.Lsp.LeanQueryModuleResponse : Type
-- Mathlib.Algebra.Lie.OfAssociative
/-- Unfortunately we now have two brackets which are not equal at reducible transparency, even
though they are equal at default transparency. We can use this lemma on rare occasions when this
matters.  -/
Module.End.instLieRingModule_eq : ∀ {R : Type u} [inst : CommRing R] {M : Type w} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  LinearMap.instLieRingModule = lieRingSelfModule
-- Init.Data.BitVec.Basic
/-- Concatenates two bitvectors using the “big-endian” convention that the more significant
input is on the left. Usually accessed via the `++` operator.

SMT-LIB name: `concat`.

Example:
 * `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
 -/
BitVec.append : {n m : ℕ} → BitVec n → BitVec m → BitVec (n + m)
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.measure_spanningSets_trim_lt_top : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} (hm : m ≤ m0) (μ : MeasureTheory.Measure α)
  [inst : MeasureTheory.SigmaFinite (μ.trim hm)] (n : ℕ), μ (MeasureTheory.spanningSets (μ.trim hm) n) < ⊤
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_fst : ∀ {X Y : AlgebraicGeometry.Scheme} (U : (X ⨿ Y).Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.coprodPresheafObjIso U).hom
      CategoryTheory.Limits.prod.fst =
    AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Limits.coprod.inl U
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ \ m₂},
  (m₁ \ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Init.Data.Order.LemmasExtra
/-- This lemma derives a `LawfulOrderMin α` instance from a property involving an `Ord α` instance.
 -/
Std.LawfulOrderMin.of_ord : ∀ (α : Type u) [inst : Ord α] [inst_1 : Min α] [inst_2 : LE α] [Std.LawfulOrderOrd α],
  (∀ (a b c : α), (compare a (b ⊓ c)).isLE = true ↔ (compare a b).isLE = true ∧ (compare a c).isLE = true) →
    (∀ (a b : α), a ⊓ b = a ∨ a ⊓ b = b) → Std.LawfulOrderMin α
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The algebra isomorphism of additive monoid algebras induced by an isomorphism of the base
algebras.  -/
AddMonoidAlgebra.mapAlgEquiv : (R : Type u_1) →
  {A : Type u_4} →
    {B : Type u_5} →
      (M : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : AddMonoid M] → (A ≃ₐ[R] B) → AddMonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra B M
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.map.match_1.eq_2 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) (a : C)
  (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (a a_1 : C) →
      (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
        motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f)
  (h_2 :
    (a : C) →
      (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f => h_1 a a_1 f
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => h_2 a x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_2 a x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_pos : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis → ∀ᶠ (x : ℝ) in Filter.atTop, 0 < m.toFun basis x
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnits_bot : ∀ {M : Type u_1} [inst : AddMonoid M], ⊥.ofAddUnits = ⊥