mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.drop.congr_simp : ∀ (p p_1 : DyckWord) (e_p : p = p_1) (i i_1 : ℕ) (e_i : i = i_1)
  (hi : List.count DyckStep.U (List.take i ↑p) = List.count DyckStep.D (List.take i ↑p)), p.drop i hi = p_1.drop i_1 ⋯
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.coeff_natTrailingDegree_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeff p.natTrailingDegree ≠ 0 ↔ p ≠ 0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.IsOver.mk : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] {f : X.RationalMap Y},
  (∃ g, AlgebraicGeometry.Scheme.PartialMap.IsOver S g ∧ g.toRationalMap = f) →
    AlgebraicGeometry.Scheme.RationalMap.IsOver S f
-- Batteries.Data.AssocList
Batteries.AssocList.length_mapVal : ∀ {α : Type u_1} {β : Type u_2} {β_1 : Type u_3} {f : α → β → β_1} {l : Batteries.AssocList α β},
  (Batteries.AssocList.mapVal f l).length = l.length
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.instBEqOfHashableOfLawfulBEq : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [Hashable α] → [LawfulBEq α] → [(k : α) → BEq (β k)] → BEq (Std.DHashMap.Raw α β)
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_mul : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f₁₂ f₂₃ : M →ₗ[R] M) (g₁₂ g₂₃ : M₂ →ₗ[R] M₂),
  f₂₃.prodMap g₂₃ * f₁₂.prodMap g₁₂ = (f₂₃ * f₁₂).prodMap (g₂₃ * g₁₂)
-- Mathlib.Geometry.RingedSpace.Basic
/-- A variant of `mem_basicOpen` with bundled `x : U`.  -/
AlgebraicGeometry.RingedSpace.mem_basicOpen' : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U),
  ↑x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f)
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- The basis of M.  -/
Module.Basis.SmithNormalForm.bM : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Submodule R M} → {ι : Type u_4} → {n : ℕ} → Module.Basis.SmithNormalForm N ι n → Module.Basis ι R M
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.epsilon_pos : 0 < Hyperreal.epsilon
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- In a T0 topological space, `diracProbaEquiv` is continuous.  -/
MeasureTheory.continuous_diracProbaEquiv : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [inst_3 : T0Space X], Continuous ⇑MeasureTheory.diracProbaEquiv
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.boundedOrder : {α : Type u_1} → [inst : LE α] → [BoundedOrder α] → BoundedOrder (Additive α)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The kernel of `biprod.fst : X ⊞ Y ⟶ X` is `Y`.  -/
CategoryTheory.Limits.kernelBiprodFstIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.kernel CategoryTheory.Limits.biprod.fst ≅ Y
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A tree is acyclic.  -/
SimpleGraph.IsTree.isAcyclic : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → G.IsAcyclic
-- Mathlib.Tactic.Simps.NotationClass
/-- Find arguments for the `One` class.  -/
Simps.findOneArgs : Simps.findArgType
-- Lean.Data.Position
Lean.Position.mk.inj : ∀ {line column line_1 column_1 : ℕ},
  { line := line, column := column } = { line := line_1, column := column_1 } → line = line_1 ∧ column = column_1
-- Mathlib.Order.SetNotation
/-- Indexed infimum  -/
iInf : {α : Type u} → {ι : Sort v} → [InfSet α] → (ι → α) → α
-- Mathlib.Topology.Order.IsLUB
IsGLB.mem_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsGLB s a → s.Nonempty → a ∈ closure s
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] [IsGalois k K]
  (φ ψ : K →+* ℂ), φ.comp (algebraMap k K) = ψ.comp (algebraMap k K) → ∃ σ, φ.comp ↑σ.symm = ψ
-- Mathlib.Order.Filter.CountablyGenerated
/-- The set of `i` that satisfy the predicate `p` is countable.  -/
Filter.IsCountableBasis.countable : ∀ {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α}, Filter.IsCountableBasis p s → (Set.ofPred p).Countable
-- Mathlib.NumberTheory.PrimeCounting
Nat.lt_of_mem_primesBelow : ∀ {p n : ℕ}, p ∈ n.primesBelow → p < n
-- Init.Meta.Defs
/-- Creates the syntax of a separated array of items. `sep` is inserted between each item from `a`, and
the result is wrapped in a null node.
 -/
Lean.Syntax.mkSep : Array Lean.Syntax → Lean.Syntax → Lean.Syntax
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.add_lt_of_neg_left : ∀ {α : Type u_1} [inst : CommSemiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] (a : α) {b : α},
  b < 0 → b + a < a
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_div : ∀ {α : Type u_1} [inst : Div α] (a b : Colex α), ofColex (a / b) = ofColex a / ofColex b
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- If `g : M ⟶ N` is a `B`-linear morphism of `B`-modules, then it induces an
`A`-linear morphism when `M` and `N` have an `A`-module structure obtained
by restricting scalars along an additive monoid morphism `A ⟶ B`.  -/
CategoryTheory.AddMod.scalarRestriction_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.AddMonObj A] [inst_5 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsAddMonHom f] (M N : D) [inst_7 : CategoryTheory.AddModObj B M]
  [inst_8 : CategoryTheory.AddModObj B N] (g : M ⟶ N) [CategoryTheory.IsAddModHom B g], CategoryTheory.IsAddModHom A g
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_inverse_obj_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B),
  ((CategoryTheory.Comma.equivProd L R).inverse.obj X).left = X.1
-- Mathlib.Probability.ProductMeasure
/-- Consider a family of probability measures. You can take their products for any finite
subfamily. This gives a projective family of measures.  -/
MeasureTheory.isProjectiveMeasureFamily_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)],
  MeasureTheory.IsProjectiveMeasureFamily fun I => MeasureTheory.Measure.pi fun i => μ ↑i
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundOptionTExceptPUnitPureOfLawfulMonad.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (r : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive r
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.exi_rat_seq_conv : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : CauSeq ℚ_[p] ⇑padicNormE) {ε : ℚ},
  0 < ε → ∃ N, ∀ i ≥ N, padicNormE (↑f i - ↑(Padic.limSeq f i)) < ε
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.matrix_strictMono_of_nonempty : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocRing R] [inst_1 : Fintype n] [h : Nonempty n],
  StrictMono (TwoSidedIdeal.matrix n)
-- Lean.Elab.Match
/-- `FVarId`s of the variables that have been generalized. We store them to clear after in each branch.  -/
Lean.Elab.Term.GeneralizeResult.toClear : Lean.Elab.Term.GeneralizeResult → Array Lean.FVarId
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.zsmul_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {x : R} (n : ℤ), x ∈ I → n • x ∈ I
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsPerfectMatching.isAlternating_symmDiff_left : ∀ {V : Type u_1} {G G' : SimpleGraph V} {M : G.Subgraph} {M' : G'.Subgraph},
  M.IsPerfectMatching → M'.IsPerfectMatching → (symmDiff M.spanningCoe M'.spanningCoe).IsAlternating M.spanningCoe
-- Init.Data.Array.Monadic
List.filterM_toArray : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool},
  Array.filterM p l.toArray = List.toArray <$> List.filterM p l
-- Lean.CoreM
/-- A variant of `tryCatch` that also catches runtime exception (see also `tryCatch` documentation).
Like `tryCatch`, this function does not catch interrupt exceptions, which are not considered runtime
exceptions.
 -/
Lean.Core.tryCatchRuntimeEx : {α : Type} → Lean.CoreM α → (Lean.Exception → Lean.CoreM α) → Lean.CoreM α
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.toPoly : Nat.Internal.Linear.ExprCnstr → Nat.Internal.Linear.PolyCnstr
-- Mathlib.Condensed.TopComparison
/-- Associate to a `(u + 1)`-small topological space the corresponding condensed set, given by
`yonedaPresheaf`.
 -/
TopCat.toCondensedSet : TopCat → CondensedSet
-- Mathlib.Order.Filter.IndicatorFunction
Monotone.mulIndicator_eventuallyEq_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} [inst : Preorder ι] [inst_1 : One β] (s : ι → Set α),
  Monotone s →
    ∀ (f : α → β) (a : α), (fun i => (s i).mulIndicator f a) =ᶠ[Filter.atTop] fun x => (⋃ i, s i).mulIndicator f a
-- Mathlib.Algebra.BigOperators.Pi
Prod.snd_sum : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {s : Finset ι}
  {f : ι → M × N}, (∑ c ∈ s, f c).2 = ∑ c ∈ s, (f c).2
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given left-open right-closed range as an array in ascending order.
 -/
Std.Roc.toArray : {α : Type u} →
  [inst : LE α] →
    [DecidableLE α] →
      [inst_2 : Std.PRange.UpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxc.IsAlwaysFinite α] → Std.Roc α → Array α
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mk'_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G), (CategoryTheory.Adjunction.mk' adj).counit = adj.counit
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
cyclotomicCharacter.eq_1 : ∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] (p : ℕ) [inst_2 : Fact (Nat.Prime p)],
  cyclotomicCharacter L p = { toFun := fun g => cyclotomicCharacter.toFun p g, map_one' := ⋯, map_mul' := ⋯ }.toHomUnits
-- Mathlib.Algebra.Lie.Killing
LieAlgebra.IsKilling.ker_killingForm_eq_bot : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L], LinearMap.ker (killingForm R L) = ⊥
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool},
  t.WF → (Std.TreeSet.Raw.filter f t).WF
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt.0.Int16.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option Int16)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.State.stxTrav : Lean.PrettyPrinter.Formatter.State → Lean.Syntax.Traverser
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Let `f` be an `n` times continuously differentiable homeomorphism of a nontrivially normed
field.  Suppose that the derivative of `f` is never equal to zero. Then `f.symm` is `n` times
continuously differentiable.

This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function.  -/
Homeomorph.contDiff_symm_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} [CompleteSpace 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 → 𝕜},
  (∀ (x : 𝕜), f' x ≠ 0) → (∀ (x : 𝕜), HasDerivAt (⇑f) (f' x) x) → ContDiff 𝕜 n ⇑f → ContDiff 𝕜 n ⇑f.symm
-- Mathlib.Topology.UniformSpace.Ultra.Completion
IsUltraUniformity.completion_iff : ∀ {X : Type u_1} [inst : UniformSpace X], IsUltraUniformity (UniformSpace.Completion X) ↔ IsUltraUniformity X
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_iff_enorm_sub_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddCommGroup E] {f : α → E} {a : Filter α} {b : E},
  Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖f e - b‖ₑ) a (nhds 0)
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CosimplicialObject.augmentedCechConerve_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom]
  {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y),
  CategoryTheory.CosimplicialObject.augmentedCechConerve.map F = CategoryTheory.Arrow.mapAugmentedCechConerve F
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- Coercion of an element of `WithAbs v.1` into the completion.  -/
NumberField.InfinitePlace.Completion.instCoeWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace : {K : Type u_1} → [inst : Field K] → (v : NumberField.InfinitePlace K) → Coe (WithAbs ↑v) v.Completion
-- Mathlib.Topology.MetricSpace.Isometry
PseudoEMetricSpace.isometry_induced : ∀ {α : Type u} {β : Type v} (f : α → β) [m : PseudoEMetricSpace β], Isometry f
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_mul : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) (x : S),
  Polynomial.eval₂ f x (p * q) = Polynomial.eval₂ f x p * Polynomial.eval₂ f x q
-- Mathlib.Algebra.Category.Ring.Limits
/-- `limit.π (F ⋙ forget SemiRingCat) j` as a `RingHom`.  -/
SemiRingCat.limitπRingHom : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J SemiRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget SemiRingCat)).sections] →
        (j : J) →
          (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget SemiRingCat))).pt →+*
            (F.comp (CategoryTheory.forget SemiRingCat)).obj j
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- If `W` is the pushout of `f, g`,
it is also the pushout of `h ≫ f, h ≫ g` for any epi `h`.  -/
CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          (h : W ⟶ X) →
            [CategoryTheory.Epi h] →
              (s : CategoryTheory.Limits.PushoutCocone f g) →
                CategoryTheory.Limits.IsColimit s →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk s.inl s.inr ⋯)
-- Lean.Message
Lean.instInhabitedBaseMessage.default : {α : Type u} → [Inhabited α] → Lean.BaseMessage α
-- Init.Data.List.Perm
List.perm_iff_count : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α},
  l₁.Perm l₂ ↔ ∀ (a : α), List.count a l₁ = List.count a l₂
-- Mathlib.LinearAlgebra.Orientation
Orientation.reindex_symm : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (M : Type u_2)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι'),
  (Orientation.reindex R M e).symm = Orientation.reindex R M e.symm
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.edist_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α}
  {x y : α}, x ∈ s → y ∈ s → edist (f x) (f y) ≤ eVariationOn f s
-- Std.Async.Process
/-- Number of swap ins or swap outs
 -/
Std.IO.Process.ResourceUsageStats.swapOperations : Std.IO.Process.ResourceUsageStats → UInt64
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forM_eq_forM_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {m' : Type w → Type w'} [inst : Monad m']
  [LawfulMonad m'] {f : (a : α) → β a → m' PUnit.{w + 1}},
  Std.DHashMap.Raw.forM f ↑m = (↑m).toList.forM fun a => f a.fst a.snd
-- Mathlib.Data.Seq.Basic
Stream'.Seq.toList_ofList : ∀ {α : Type u} (l : List α), (↑l).toList ⋯ = l
-- Mathlib.Algebra.Category.Ring.EqualizerPushout
/-- A regular epimorphism structure on a map `f : S ⟶ R` in `CommRingCatᵒᵖ` with
faithfully flat `f.unop.hom : R.unop ⟶ S.unop`.  -/
CommRingCat.Opposite.regularEpiOfFaithfullyFlat : ∀ {R S : CommRingCatᵒᵖ} (f : S ⟶ R), (CommRingCat.Hom.hom f.unop).FaithfullyFlat → CategoryTheory.IsRegularEpi f
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.listTake_succ_alternatingWord : ∀ {B : Type u_1} (i j : B) (p k : ℕ),
  k + 1 < 2 * p →
    List.take (k + 1) (CoxeterSystem.alternatingWord i j (2 * p)) =
      i :: List.take k (CoxeterSystem.alternatingWord j i (2 * p))
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.instLawfulOperatorMkAtomCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α (fun x => α) Std.Sat.AIG.mkAtomCached
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handlePlainTermGoal : Lean.Lsp.PlainTermGoalParams → Lean.Server.RequestM (Lean.Server.RequestTask (Option Lean.Lsp.PlainTermGoal))
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.domLCongr_refl : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Finsupp.domLCongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M)
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.map_add_atTop_eq : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] [IsDirectedOrder α] (k : α),
  Filter.map (fun a => a + k) Filter.atTop = Filter.atTop
-- Lean.Message
Lean.ToMessageData.mk : {α : Type} → (α → Lean.MessageData) → Lean.ToMessageData α
-- Mathlib.MeasureTheory.Covering.Vitali
/-- **Vitali covering theorem**: given a set `t` of subsets of a type, one may extract a disjoint
subfamily `u` such that the `τ`-enlargement of this family covers all elements of `t`, where `τ > 1`
is any fixed number.

When `t` is a family of balls, the `τ`-enlargement of `ball x r` is `ball x ((1+2τ) r)`. In general,
it is expressed in terms of a function `δ` (think "radius" or "diameter"), positive and bounded on
all elements of `t`. The condition is that every element `a` of `t` should intersect an
element `b` of `u` of size larger than that of `a` up to `τ`, i.e., `δ b ≥ δ a / τ`.

We state the lemma slightly more generally, with an indexed family of sets `B a` for `a ∈ t`, for
wider applicability.
 -/
Vitali.exists_disjoint_subfamily_covering_enlargement : ∀ {α : Type u_1} {ι : Type u_2} (B : ι → Set α) (t : Set ι) (δ : ι → ℝ) (τ : ℝ),
  1 < τ →
    (∀ a ∈ t, 0 ≤ δ a) →
      ∀ (R : ℝ),
        (∀ a ∈ t, δ a ≤ R) →
          (∀ a ∈ t, (B a).Nonempty) →
            ∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.inductionOn : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M},
  IsTensorProduct f →
    ∀ {motive : M → Prop} (m : M),
      motive 0 →
        (∀ (x : M₁) (y : M₂), motive ((f x) y)) → (∀ (x y : M), motive x → motive y → motive (x + y)) → motive m
-- Mathlib.CategoryTheory.Pi.Basic
_private.Mathlib.CategoryTheory.Pi.Basic.0.CategoryTheory.Pi.sumElimCategory.match_19.eq_2 : ∀ {I J : Type u_1} (motive : I ⊕ J → Sort u_2) (j : J) (h_1 : (i : I) → motive (Sum.inl i))
  (h_2 : (j : J) → motive (Sum.inr j)),
  (match Sum.inr j with
    | Sum.inl i => h_1 i
    | Sum.inr j => h_2 j) =
    h_2 j
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_cosh : Measurable Complex.cosh
-- Mathlib.Data.Nat.Nth
Nat.subset_range_nth : ∀ {p : ℕ → Prop}, Set.ofPred p ⊆ Set.range (Nat.nth p)
-- Mathlib.Topology.Homeomorph.Defs
/-- Composition of two homeomorphisms.  -/
Homeomorph.trans : {X : Type u_1} →
  {Y : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] → [inst_2 : TopologicalSpace Z] → X ≃ₜ Y → Y ≃ₜ Z → X ≃ₜ Z
-- Init.Control.Lawful.Instances
OptionT.seqRight_eq : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β),
  x *> y = Function.const α id <$> x <*> y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_eq_get!_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.get! a = (m.get? a).get!
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.mem_compactConvergence_entourage_iff : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] (X : Set (C(α, β) × C(α, β))),
  X ∈ uniformity C(α, β) ↔ ∃ K V, IsCompact K ∧ V ∈ uniformity β ∧ {fg | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V} ⊆ X
-- Mathlib.Logic.Equiv.Fintype
Equiv.Perm.viaFintypeEmbedding.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (e : Equiv.Perm α) (f : α ↪ β),
  e.viaFintypeEmbedding f = e.extendDomain f.toEquivRange
-- Init.Data.BitVec.Lemmas
/-- A bitvector interpreted as a natural number is greater than or equal to `2 ^ i` if and only if
there exists at least one bit with `true` value at position `i` or higher.  -/
BitVec.le_toNat_iff_getLsbD_eq_true : ∀ {w i : ℕ} {x : BitVec w}, i < w → (2 ^ i ≤ x.toNat ↔ ∃ k, x.getLsbD (i + k) = true)
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.analyticAt_bilinear : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  AnalyticAt 𝕜 (fun x => (f x.1) x.2) x
-- Init.Data.List.SplitOn.Basic
/-- Split a list at every element satisfying a predicate, and then prepend `acc.reverse` to the
first element of the result.

* `[1, 1, 2, 3, 2, 4, 4].splitOnPPrepend (· == 2) [0, 5] = [[5, 0, 1, 1], [3], [4, 4]]`
 -/
List.splitOnPPrepend : {α : Type u_1} → (α → Bool) → List α → List α → List (List α)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insertWith.valid_aux : ∀ {α : Type u_1} [inst : Preorder α] [Std.Total fun x1 x2 => x1 ≤ x2] [inst_2 : DecidableLE α] (f : α → α) (x : α),
  (∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) →
    ∀ {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
      Ordnode.Valid' o₁ t o₂ →
        Ordnode.nil.Bounded o₁ ↑x →
          Ordnode.nil.Bounded (↑x) o₂ →
            Ordnode.Valid' o₁ (Ordnode.insertWith f x t) o₂ ∧ Ordnode.Raised t.size (Ordnode.insertWith f x t).size
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM.run : {α : Type} → ℕ → Lean.Meta.Grind.AC.ACM α → Lean.Meta.Grind.GoalM α
-- Mathlib.LinearAlgebra.StdBasis
Pi.basisFun.eq_1 : ∀ (R : Type u_2) (η : Type u_4) [inst : Semiring R] [inst_1 : Finite η],
  Pi.basisFun R η = Module.Basis.ofEquivFun (LinearEquiv.refl R (η → R))
-- Lean.Elab.Do.Basic
/-- Create the `Context` for `do` elaboration from the given expected type of a `do` block.  -/
Lean.Elab.Do.mkContext : Option Lean.Expr → optParam Lean.Elab.Do.DoOps Lean.Elab.Do.DoOps.default → Lean.Elab.TermElabM Lean.Elab.Do.Context
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.refl : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
  CategoryTheory.FreeMonoidalCategory.HomEquiv f f
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_of_isZero_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.Limits.IsZero S.X₂ → S.Exact