mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- A bounded convergence theorem for a finite measure:
If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a
limit, then their integrals against the finite measure tend to the integral of the limit.
This formulation assumes:
* the functions tend to a limit along a countably generated filter;
* the limit is in the almost everywhere sense;
* boundedness holds almost everywhere;
* integration is the pairing against non-negative continuous test functions
  (`MeasureTheory.FiniteMeasure.testAgainstNN`).

A related result using `MeasureTheory.lintegral` for integration is
`MeasureTheory.FiniteMeasure.tendsto_lintegral_nn_filter_of_le_const`.
 -/
MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_filter_of_le_const : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2}
  {L : Filter ι} [L.IsCountablyGenerated] {μ : MeasureTheory.FiniteMeasure Ω}
  {fs : ι → BoundedContinuousFunction Ω NNReal} {c : NNReal},
  (∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, (fs i) ω ≤ c) →
    ∀ {f : BoundedContinuousFunction Ω NNReal},
      (∀ᵐ (ω : Ω) ∂↑μ, Filter.Tendsto (fun i => (fs i) ω) L (nhds (f ω))) →
        Filter.Tendsto (fun i => μ.testAgainstNN (fs i)) L (nhds (μ.testAgainstNN f))
-- Batteries.Recycling.RBTree.WF
/-- The `insert` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α} {v : α},
  RBTree.RBNode.Ordered cmp t → RBTree.RBNode.Ordered cmp (RBTree.RBNode.insert cmp t v)
-- Batteries.Recycling.RBTree.WF
/-- The balance invariant of the `ins` function.
The result of inserting into the tree either yields a balanced tree,
or a tree which is almost balanced except that it has a red-red violation at the root.
 -/
RBTree.RBNode.Balanced.ins : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} (cmp : α → α → Ordering) (v : α) {t : RBTree.RBNode α},
  t.Balanced c n → RBTree.RBNode.RedRed (t.isRed = RBTree.RBColor.red) (RBTree.RBNode.ins cmp v t) n
-- Lean.Elab.Tactic.Induction
/-- Elaborates the term in the `using` clause. We want to allow parameters to be instantiated
(e.g. `using foo (p := …)`), but preserve other parameters, like the motives, as parameters,
without turning them into MVars. So this uses `abstractMVars` at the end. This is inspired by
`Lean.Elab.Tactic.addSimpTheorem`.

It also elaborates without `heedElabAsElim` so that users can use constants that are marked
`elabAsElim` in the `using` clause`.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.elabTermForElim : Lean.Syntax → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Analysis.Complex.Order
/-- Extension for the `positivity` tactic: `Complex.ofReal` is positive/nonnegative/nonzero if its
input is.  -/
Mathlib.Meta.Positivity.evalComplexOfReal : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Sites.InducedTopology
CategoryTheory.Functor.inducedTopology_le_restrictedTopology : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D},
  F.inducedTopology K ≤ F.restrictedTopology K
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.mk.sizeOf_spec : ∀ (toList : List DyckStep) (count_U_eq_count_D : List.count DyckStep.U toList = List.count DyckStep.D toList)
  (count_D_le_count_U :
    ∀ (i : ℕ), List.count DyckStep.D (List.take i toList) ≤ List.count DyckStep.U (List.take i toList)),
  sizeOf { toList := toList, count_U_eq_count_D := count_U_eq_count_D, count_D_le_count_U := count_D_le_count_U } =
    1 + sizeOf toList + sizeOf count_U_eq_count_D
-- Mathlib.Control.Bifunctor
Bifunctor.const : Bifunctor Functor.Const
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.IsExtension : ∀ {R : Type u_1} {N : Type u_2} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing N] [inst_2 : LieAlgebra R N]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (self : LieAlgebra.Extension R N M),
  LieAlgebra.IsExtension self.incl self.proj
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.implicitFunctionDataOfProdDomain.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u u_1 : E₁ × E₂} (e_u : u = u_1) {f f_1 : E₁ × E₂ → F}
  (e_f : f = f_1) {f'u f'u_1 : E₁ × E₂ →L[𝕜] F} (e_f'u : f'u = f'u_1) (dfu : HasStrictFDerivAt f f'u u)
  (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  dfu.implicitFunctionDataOfProdDomain if₂u = ⋯.implicitFunctionDataOfProdDomain ⋯
-- Mathlib.Computability.RegularExpressions
RegularExpression.instAdd : {α : Type u_1} → Add (RegularExpression α)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} {fallback : β} (h : m.WF),
  (Std.HashMap.Raw.filter f m).getD k fallback = (m[k]?.pfilter fun x h' => f (m.getKey k ⋯) x).getD fallback
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.totalSpaceMk_preimage_source : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle R F E) (b : B), Bundle.TotalSpace.mk b ⁻¹' (a.pretrivializationAt b).source = Set.univ
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurable_derivWithin_Ioi : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F]
  [inst_3 : MeasurableSpace F] [BorelSpace F], Measurable fun x => derivWithin f (Set.Ioi x) x
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply : ∀ (X : Type (u + 1)) (S : Profinite)
  (s : CategoryTheory.Limits.Cocone (S.diagram.op.comp (Condensed.locallyConstantPresheaf X)))
  (i : DiscreteQuotient ↑S.toTop) (f : LocallyConstant (↑(S.diagram.obj i).toTop) X),
  (CategoryTheory.ConcreteCategory.hom ((Condensed.isColimitLocallyConstantPresheafDiagram X S).desc s))
      (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app i).hom) f) =
    (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op i))) f
-- Aesop.Tree.Tracing
_private.Aesop.Tree.Tracing.0.Aesop.toYesNo : Bool → String
-- Init.Conv
/-- Lifts `let` and `have` expressions within the target expression as far out as possible.
This is the conv mode version of the `lift_lets` tactic.
 -/
Lean.Parser.Tactic.Conv.liftLets : Lean.ParserDescr
-- Lean.Elab.DocString
Lean.Doc.SuggestionMode.batch.sizeOf_spec : sizeOf Lean.Doc.SuggestionMode.batch = 1
-- Init.Grind.Module.Basic
/-- A type with zero and addition,
where addition is commutative and associative,
and the zero is the right identity for addition.  -/
Lean.Grind.AddCommMonoid : Type u → Type u
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_apply_eq : ∀ {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₂) {x : M₂}
  {y : M}, e.symm x = y ↔ x = e y
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LClause.mk : Array ℤ → Lean.Expr → ℕ → Mathlib.Tactic.Sat.LClause
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.mk.sizeOf_spec : ∀ {S : Type u_2} {M : Type u_3} [inst : VAdd S M] [inst_1 : SizeOf S] [inst_2 : SizeOf M] (toSetoid : Setoid M)
  (vadd : ∀ (s : S) {x y : M}, toSetoid x y → toSetoid (s +ᵥ x) (s +ᵥ y)),
  sizeOf { toSetoid := toSetoid, vadd := vadd } = 1 + sizeOf toSetoid
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isBigO_comp_ofReal_nhds_ne : ∀ {f g : ℂ → ℂ} {x : ℝ}, f =O[nhdsWithin ↑x {↑x}ᶜ] g → (fun y => f ↑y) =O[nhdsWithin x {x}ᶜ] fun y => g ↑y
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_eq_getValueCast! : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Inhabited β] {l : List ((_ : α) × β)}
  {a : α}, Std.Internal.List.getValue! a l = Std.Internal.List.getValueCast! a l
-- Init.System.ST
/-- Creates a `MonadStateOf` instance from a reference cell.

This allows programs written against the [state monad](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=state-monads) API to
be executed using a mutable reference cell to track the state.
 -/
ST.Ref.toMonadStateOf : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ α → MonadStateOf α m
-- Std.Time.Format.DateFormat
/-- Narrow PM marker (used by `aaaaa`).
 -/
Std.Time.DateFormatSymbols.pmNarrow : Std.Time.DateFormatSymbols → String
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.ofExact_var : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst_1 : AddCommGroup M₁]
  [inst_2 : Module A M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] [inst_5 : AddCommGroup M₃]
  [inst_6 : Module A M₃] {f : M₁ →ₗ[A] M₂} {g : M₂ →ₗ[A] M₃} (pres₂ : Module.Presentation A M₂) {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g)
  (hg₁ : Submodule.span A (Set.range g₁) = ⊤) (g_1 : (pres₂.cokernel data hg₁).G),
  (pres₂.ofExact data hfg hg hg₁).var g_1 = g (pres₂.var g_1)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- Any action is 0-pretransitive.  -/
MulAction.is_zero_pretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {n : Type u_5} [IsEmpty n],
  MulAction.IsPretransitive G (n ↪ α)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_same : ∀ {w : ℕ} (a : BitVec w), a + a = a * 2#w
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime : ∀ {α : Type u_1} {f : α → α} {x : α} {g : α → α},
  Function.Commute f g →
    (Function.minimalPeriod f x).Coprime (Function.minimalPeriod g x) →
      Function.minimalPeriod (f ∘ g) x = Function.minimalPeriod f x * Function.minimalPeriod g x
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_c_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c ≠ 0 → P.toPoly.natDegree = 1
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instSemiring : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → Semiring (TensorProduct R A B)
-- Std.Time.Format
/-- Parses a `String` in the `Time12Hour` or `Time24Hour` format and returns a `PlainTime`.
 -/
Std.Time.PlainTime.parse : String → Except String Std.Time.PlainTime
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
summable_finsetProd_of_summable_nonneg : ∀ {ι : Type u_1} {f : ι → ℝ}, (∀ (i : ι), 0 ≤ f i) → Summable f → Summable fun s => ∏ i ∈ s, f i
-- Lean.Attributes
Lean.instInhabitedParametricAttribute : {a : Type} → Inhabited (Lean.ParametricAttribute a)
-- Lean.Parser.Module
_private.Lean.Parser.Module.0.Lean.Parser.mkErrorMessage : Lean.Parser.InputContext → String.Pos.Raw → Lean.Parser.SyntaxStack → Lean.Parser.Error → Lean.Message
-- Mathlib.Logic.Godel.GodelBetaFunction
/-- Gödel's Beta Function. This is similar to `(Encodable.decodeList)[i]`, but it is easier to
prove that it is arithmetically definable.  -/
Nat.beta : ℕ → ℕ → ℕ
-- Mathlib.Topology.UniformSpace.Ultra.Constructions
SetRel.isTrans_entourageProd : ∀ {X : Type u_1} {Y : Type u_2} {s : SetRel X X} {t : SetRel Y Y} [s.IsTrans] [t.IsTrans], (entourageProd s t).IsTrans
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- Being `Cⁿ` in the model space is a local property, invariant under `C^n` maps. Therefore,
it lifts nicely to manifolds.  -/
contDiffWithinAt_localInvariantProp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {E' : Type u_5}
  [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} (n : WithTop ℕ∞),
  (contDiffGroupoid n I).LocalInvariantProp (contDiffGroupoid n I') (ContDiffWithinAtProp I I' n)
-- Init.Data.String.Lemmas.Iterate
String.toList_positions : ∀ {s : String}, s.positions.toList = String.Model.positionsFrom s.startPos
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The isomorphism between the specified limit and the specified colimit for
a functor with a bilimit.  -/
CategoryTheory.Limits.biproductIso : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (F : J → C) → [inst_2 : CategoryTheory.Limits.HasBiproduct F] → ∏ᶜ F ≅ ∐ F
-- Mathlib.Logic.Basic
/-- In most cases, we should not have global instances of `Fact`; typeclass search is not an
advanced proof search engine, and adding any such instance has the potential to cause
slowdowns everywhere. We instead declare them as lemmata and make them local instances as required.
 -/
LibraryNote.«fact_non-instances» : Batteries.Util.LibraryNote
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.coprod.inl_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} (x : C),
  CategoryTheory.FunctorToTypes.coprod.inl.app x = TypeCat.ofHom fun x_1 => Sum.inl x_1
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- A square of squares between right adjoints can be composed by iterating vertical and horizontal
composition.
 -/
CategoryTheory.Bicategory.rightAdjointSquare.comp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d e f x y z : B} →
      {g₁ : a ⟶ d} →
        {h₁ : b ⟶ e} →
          {k₁ : c ⟶ f} →
            {g₂ : d ⟶ x} →
              {h₂ : e ⟶ y} →
                {k₂ : f ⟶ z} →
                  {r₁ : b ⟶ a} →
                    {r₂ : c ⟶ b} →
                      {r₃ : e ⟶ d} →
                        {r₄ : f ⟶ e} →
                          {r₅ : y ⟶ x} →
                            {r₆ : z ⟶ y} →
                              (CategoryTheory.CategoryStruct.comp r₁ g₁ ⟶ CategoryTheory.CategoryStruct.comp h₁ r₃) →
                                (CategoryTheory.CategoryStruct.comp r₂ h₁ ⟶ CategoryTheory.CategoryStruct.comp k₁ r₄) →
                                  (CategoryTheory.CategoryStruct.comp r₃ g₂ ⟶
                                      CategoryTheory.CategoryStruct.comp h₂ r₅) →
                                    (CategoryTheory.CategoryStruct.comp r₄ h₂ ⟶
                                        CategoryTheory.CategoryStruct.comp k₂ r₆) →
                                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp r₂ r₁)
                                          (CategoryTheory.CategoryStruct.comp g₁ g₂) ⟶
                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp k₁ k₂)
                                          (CategoryTheory.CategoryStruct.comp r₆ r₅))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- Constructor for morphisms from `(t.truncGT n₀).obj Y`.  -/
CategoryTheory.Triangulated.TStructure.descTruncGT : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                {X Y : C} → (X ⟶ Y) → (n₀ n₁ : ℤ) → n₀ + 1 = n₁ → [t.IsGE Y n₁] → (t.truncGT n₀).obj X ⟶ Y
-- Mathlib.Data.Finset.Max
/-- Let `s` be a finset in a linear order. Then `s.max` is the maximum of `s` if `s` is not empty,
and `⊥` otherwise. It belongs to `WithBot α`. If you want to get an element of `α`, see
`s.max'`.  -/
Finset.max : {α : Type u_2} → [LinearOrder α] → Finset α → WithBot α
-- Aesop.Options.Public
Aesop.Strategy.bestFirst.sizeOf_spec : sizeOf Aesop.Strategy.bestFirst = 1
-- Mathlib.NumberTheory.Chebyshev
Nat.lcmUpto_ne_zero : ∀ (n : ℕ), n.lcmUpto ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.Limits.Cone.π.hcongr_6 : ∀ (J J' : Type u₁),
  J = J' →
    ∀ (inst : CategoryTheory.Category.{v₁, u₁} J) (inst' : CategoryTheory.Category.{v₁, u₁} J'),
      inst ≍ inst' →
        ∀ (C C' : Type u₃),
          C = C' →
            ∀ (inst_1 : CategoryTheory.Category.{v₃, u₃} C) (inst'_1 : CategoryTheory.Category.{v₃, u₃} C'),
              inst_1 ≍ inst'_1 →
                ∀ (F : CategoryTheory.Functor J C) (F' : CategoryTheory.Functor J' C'),
                  F ≍ F' →
                    ∀ (self : CategoryTheory.Limits.Cone F) (self' : CategoryTheory.Limits.Cone F'),
                      self ≍ self' → self.π ≍ self'.π
-- Lean.Elab.App
/-- Positions of "major" parameters (those that should be eagerly elaborated
because they can contribute to the motive inference procedure).
All parameters that are neither the motive nor a major parameter are "minor" parameters.
The major parameters include all of the parameters that transitively appear in the motive's arguments,
as well as "first-order" arguments that include such parameters,
since they too can help with elaborating discriminants.

For example, in the following theorem the argument `h : a = b`
should be elaborated eagerly because it contains `b`, which occurs in `motive b`.
```
theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b
```
For another example, the term `isEmptyElim (α := α)` is an underapplied eliminator, and it needs
argument `α` to be elaborated eagerly to create a type-correct motive.
```
def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ...
example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α)
```
 -/
Lean.Elab.Term.ElabElimInfo.majorsPos : Lean.Elab.Term.ElabElimInfo → Array ℕ
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.add : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instVAdd' : {β : Type u_2} → {α : Type u_1} → [VAdd β α] → VAdd βᵒᵈ α
-- Mathlib.Topology.Separation.CompletelyRegular
CompletelyRegularSpace.completely_regular_isOpen : ∀ {X : Type u} [inst : TopologicalSpace X] [CompletelyRegularSpace X] (x : X) (K : Set X),
  IsOpen K → x ∈ K → ∃ f, Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 Kᶜ
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.ofDescentData_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)) (D : F.DescentData f)
  (i₁ i₂ : ι),
  (CategoryTheory.Pseudofunctor.DescentData'.ofDescentData sq sq₃ D).hom i₁ i₂ =
    D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.comp_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type u_1} [inst_2 : TopologicalSpace Z] {T : Type u_2} [inst_3 : TopologicalSpace T]
  (g : Topology.ContinuousMapGeneratedBy X Y Z) (f : Topology.ContinuousMapGeneratedBy X T Y) (a : T),
  (g.comp f) a = (g.toFun ∘ f.toFun) a
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α],
  MulAction.orbitRel G α = { r := fun a b => a ∈ MulAction.orbit G b, iseqv := ⋯ }
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sections.mk.injEq : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  (val : (i : J.L) → I.left i)
  (property :
    ∀ (r : J.R),
      (CategoryTheory.ConcreteCategory.hom (I.fst r)) (val (J.fst r)) =
        (CategoryTheory.ConcreteCategory.hom (I.snd r)) (val (J.snd r)))
  (val_1 : (i : J.L) → I.left i)
  (property_1 :
    ∀ (r : J.R),
      (CategoryTheory.ConcreteCategory.hom (I.fst r)) (val_1 (J.fst r)) =
        (CategoryTheory.ConcreteCategory.hom (I.snd r)) (val_1 (J.snd r))),
  ({ val := val, property := property } = { val := val_1, property := property_1 }) = (val = val_1)
-- Std.Data.ExtHashSet.Basic
/-- Inserts the given element into the set. If the hash set already contains an element that is
equal (with regard to `==`) to the given element, then the hash set is returned unchanged.

Note: this non-replacement behavior is true for `ExtHashSet` and `ExtHashSet.Raw`.
The `insert` function on `ExtHashMap`, `DExtHashMap`, `ExtHashMap.Raw` and `DExtHashMap.Raw` behaves
differently: it will overwrite an existing mapping.
 -/
Std.ExtHashSet.insert : {α : Type u} →
  {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → α → Std.ExtHashSet α
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.AContext.mk.injEq : ∀ (fvars : Array Lean.Expr) (propToFVar : Lean.ExprMap Lean.Expr) (depth : ℕ) (initLCtx : Lean.LocalContext)
  (config : Batteries.Tactic.GeneralizeProofs.Config) (fvars_1 : Array Lean.Expr)
  (propToFVar_1 : Lean.ExprMap Lean.Expr) (depth_1 : ℕ) (initLCtx_1 : Lean.LocalContext)
  (config_1 : Batteries.Tactic.GeneralizeProofs.Config),
  ({ fvars := fvars, propToFVar := propToFVar, depth := depth, initLCtx := initLCtx, config := config } =
      { fvars := fvars_1, propToFVar := propToFVar_1, depth := depth_1, initLCtx := initLCtx_1, config := config_1 }) =
    (fvars = fvars_1 ∧ propToFVar = propToFVar_1 ∧ depth = depth_1 ∧ initLCtx = initLCtx_1 ∧ config = config_1)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Concyclic.Coplanar : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P}, EuclideanGeometry.Concyclic ps → Coplanar ℝ ps
-- Mathlib.NumberTheory.SmoothNumbers
/-- If `p` is a prime and `n` is `s`-factored, then every product `p^e * n`
is `s ∪ {p}`-factored.  -/
Nat.pow_mul_mem_factoredNumbers : ∀ {s : Finset ℕ} {p n : ℕ},
  Nat.Prime p → ∀ (e : ℕ), n ∈ Nat.factoredNumbers s → p ^ e * n ∈ Nat.factoredNumbers (insert p s)
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.mFourierCoeff_toLp : ∀ {d : Type u_1} [inst : Fintype d] (f : C(UnitAddTorus d, ℂ)) (n : d → ℤ),
  UnitAddTorus.mFourierCoeff (↑↑((ContinuousMap.toLp 2 MeasureTheory.volume ℂ) f)) n = UnitAddTorus.mFourierCoeff (⇑f) n
-- Std.Data.Internal.List.Associative
Std.Internal.List.values_nil : ∀ {α : Type u} {β : Type v}, Std.Internal.List.values [] = []
-- Init.Data.UInt.Lemmas
USize.lt_trans : ∀ {a b c : USize}, a < b → b < c → a < c
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_le_of_sum_le : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : Preorder α] [inst_1 : AddCommMonoid α]
  [inst_2 : TopologicalSpace α] {a c : α} {f : ι → α} [ClosedIicTopology α] [L.NeBot],
  HasSum f a L → (∀ (s : Finset ι), ∑ i ∈ s, f i ≤ c) → a ≤ c
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.length_dropUntil : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] (p : G.Walk u v) (h : w ∈ p.support),
  (p.dropUntil w h).length = p.length - List.idxOf w p.support