mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
AEMeasurable.enorm : ∀ {β : Type u_2} {ε : Type u_5} [inst : MeasurableSpace ε] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε]
  [OpensMeasurableSpace ε] [inst_4 : MeasurableSpace β] {f : β → ε} {μ : MeasureTheory.Measure β},
  AEMeasurable f μ → AEMeasurable (fun x => ‖f x‖ₑ) μ
-- Batteries.CodeAction.Attr
/-- The declaration to tag  -/
Batteries.CodeAction.TacticCodeActionEntry.declName : Batteries.CodeAction.TacticCodeActionEntry → Lean.Name
-- Lean.Elab.MutualInductive
Lean.Elab.Command.PreElabHeaderResult.mk.sizeOf_spec : ∀ (view : Lean.Elab.Command.InductiveView) (levelNames : List Lean.Name) (numParams : ℕ) (type : Lean.Expr)
  (origParams : Array Lean.Expr),
  sizeOf { view := view, levelNames := levelNames, numParams := numParams, type := type, origParams := origParams } =
    1 + sizeOf view + sizeOf levelNames + sizeOf numParams + sizeOf type + sizeOf origParams
-- Mathlib.Analysis.Convex.SpecificFunctions.Deriv
/-- `x^n`, `n : ℕ` is strictly convex on the whole real line whenever `n ≠ 0` is even.  -/
Even.strictConvexOn_pow : ∀ {n : ℕ}, Even n → n ≠ 0 → StrictConvexOn ℝ Set.univ fun x => x ^ n
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_δ_self' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 3)},
  j = i.castSucc →
    CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ j) = CategoryTheory.CategoryStruct.comp (X.δ i) (X.δ i.succ)
-- Init.Data.Nat.Basic
Nat.succ_sub : ∀ {m n : ℕ}, n ≤ m → m.succ - n = (m - n).succ
-- Lean.Meta.Tactic.Generalize
Lean.Meta.instInhabitedGeneralizeArg.default : Lean.Meta.GeneralizeArg
-- Aesop.Options.Public
Aesop.instBEqOptions.beq : Aesop.Options → Aesop.Options → Bool
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.eq_top_of_isUnit_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) {x : α}, x ∈ I → IsUnit x → I = ⊤
-- Mathlib.Data.Prod.Lex
Prod.Lex.toLex_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β], Monotone ⇑toLex
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsPosSemidef.isSymm : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : LE R]
  {B : LinearMap.BilinForm R M}, B.IsPosSemidef → B.IsSymm
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField : ∀ (k : Type u_1) (K : Type u_2) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L : FiniteGaloisIntermediateField k K), IsGalois k ↥L.toIntermediateField
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_pred : ∀ {n : ℕ} (i j : Fin (n + 3)) (h : i < j),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE ⋯) (SSet.stdSimplex.faceSingletonComplIso i).inv =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.facePairComplIso i j h).inv (SSet.stdSimplex.δ (j.pred ⋯))
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsFiniteKernel.map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] (f : β → γ),
  ProbabilityTheory.IsFiniteKernel (κ.map f)
-- Mathlib.Order.Concept
lowerPolar_anti : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop), Antitone (lowerPolar r)
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_symm_neg : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommGroup M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubgroupClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] (x : DirectSum ι fun i => ↥(ℳ i)),
  (DirectSum.decompose ℳ).symm (-x) = -(DirectSum.decompose ℳ).symm x
-- Mathlib.Topology.Constructions.SumProd
/-- `{*} × X` is homeomorphic to `X`.  -/
Homeomorph.punitProd : (X : Type u) → [inst : TopologicalSpace X] → PUnit.{u_7 + 1} × X ≃ₜ X
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.isIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y), CategoryTheory.IsIso e.hom
-- Init.Data.Array.Lemmas
/-- Variant of `append_inj` instead requiring equality of the sizes of the second arrays.  -/
Array.append_inj' : ∀ {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → ys₁.size = ys₂.size → xs₁ = xs₂ ∧ ys₁ = ys₂
-- Mathlib.Analysis.Normed.Lp.LpEquiv
Equiv.lpPiLp.eq_1 : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Finite α],
  Equiv.lpPiLp = { toFun := fun f => WithLp.toLp p ↑f, invFun := fun f => ⟨f.ofLp, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.hom_ext : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} {f g : Monoid.PushoutI φ →* K},
  (∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)) →
    f.comp (Monoid.PushoutI.base φ) = g.comp (Monoid.PushoutI.base φ) → f = g
-- Init.PropLemmas
exists_prop : ∀ {b a : Prop}, (∃ (_ : a), b) ↔ a ∧ b
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.coconeMorphism.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (j : J),
  AddMonCat.FilteredColimits.coconeMorphism F j =
    AddMonCat.ofHom
      {
        toFun :=
          ⇑(CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget AddMonCat))).ι.app j)),
        map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Elab.Tactic.Try
/-- `evalSuggest` for `tac1 <;> tac2`  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestChain : Lean.TSyntax `tactic → Lean.TSyntax `tactic → Lean.Elab.Tactic.Try.TryTacticM (Lean.TSyntax `tactic)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_div : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Div β]
  [inst_3 : ContinuousDiv β] (f g : C(α, β)), ⇑(f / g) = ⇑f / ⇑g
-- Init.Data.Array.Monadic
Array.foldrM_attachWith : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : ℕ} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  {q : α → Prop} (H : ∀ a ∈ xs, q a) {f : { x // q x } → β → m β} {b : β} {w : start = xs.size},
  Array.foldrM f b (xs.attachWith q H) start = Array.foldrM (fun a acc => f ⟨↑a, ⋯⟩ acc) b xs.attach
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.compLeft_apply : ∀ {α : Type u_5} {β : Type u_6} [inst : Add α] [inst_1 : Add β] (f : α →ₙ+ β) (I : Type u_7) (h : I → α) (a : I),
  (f.compLeft I) h a = (⇑f ∘ h) a
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.mul_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), (a * b).toProd.1 = a.toProd.1 * b.toProd.1
-- Mathlib.Order.Filter.Pointwise
Filter.isScalarTower : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α β] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [IsScalarTower α β γ], IsScalarTower α β (Filter γ)
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.closure_eq_right : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.IsBasis I (M.closure X) → M.closure I = M.closure X
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern.mk.sizeOf_spec : ∀ (fvarId : Lean.FVarId) (idx : ℕ), sizeOf { fvarId := fvarId, idx := idx } = 1 + sizeOf fvarId + sizeOf idx
-- Lean.LocalContext
Lean.mkLetDeclEx : ℕ → Lean.FVarId → Lean.Name → Lean.Expr → Lean.Expr → Lean.LocalDecl
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.instIsEquivalenceFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  (CategoryTheory.ShrinkHoms.functor C).IsEquivalence
-- Mathlib.Algebra.Ring.Torsion
MonoidHom.map_sub_swap : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : Monoid M] [IsMulTorsionFree M] (f : R →* M) (x y : R),
  f (x - y) = f (y - x)
-- Mathlib.RingTheory.Ideal.Over
Ideal.bot_liesOver_bot : ∀ (A : Type u_2) (B : Type u_3) [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : Algebra A B] [FaithfulSMul A B],
  ⊥.LiesOver ⊥
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
/-- If `x ∈ [a, b]`, then the distance between `c` and `b` is less than or equal to
that of `a` and `b`  -/
Set.abs_sub_right_of_mem_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a b c : α},
  c ∈ Set.uIcc a b → |b - c| ≤ |b - a|
-- Mathlib.CategoryTheory.ComposableArrows.Basic
Fin.natAddLEFunctor_obj_val : ∀ {n k l : ℕ} (h : k + l ≤ n) (x : Fin (l + 1)), ↑((Fin.natAddLEFunctor h).obj x) = k + ↑x
-- Batteries.Data.AssocList
/-- `O(n)`. Returns the first value in the list whose key is equal to `a`.  -/
Batteries.AssocList.find? : {α : Type u_1} → {β : Type u_2} → [BEq α] → α → Batteries.AssocList α β → Option β
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_ofIntLE : ∀ {n : ℤ} (h₁ : Int32.minValue.toInt ≤ n) (h₂ : n ≤ Int32.maxValue.toInt),
  (Int32.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.instIsAffineHomMapOverSchemeOpensDiagram : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {i : I} (U : (D.obj i).Opens)
  {j k : CategoryTheory.Over i} (f : j ⟶ k),
  AlgebraicGeometry.IsAffineHom ((AlgebraicGeometry.opensDiagram D i U).map f)
-- Mathlib.Topology.Algebra.UniformConvergence
instAddUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Add β], instAddUniformFun = { add := instAddUniformFun._aux_1 }
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- `origin` is mainly relevant for producing trace messages.
It is also viewed an `id` used to "erase" `simp` theorems from `SimpTheorems`.
 -/
Lean.Meta.SimpTheorem.origin : Lean.Meta.SimpTheorem → Lean.Meta.Origin
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.div_lt_const : ∀ {α : Type u_1} {b c : α} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α],
  b < c → ∀ {a : α}, 0 < a → b / a < c / a
-- Mathlib.Control.Fold
Monoid.foldrM.ofFreeMonoid : {m : Type u → Type u} →
  [inst : Monad m] → {α β : Type u} → [inst_1 : LawfulMonad m] → (α → β → m β) → FreeMonoid α →* Monoid.foldrM m β
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α}
  {k : α},
  ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m (k :: l)) =
    ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit (m.insertIfNew k ()) l)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.injective : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β),
  Function.Injective ⇑e
-- Lean.Level
Lean.Level.hasMVar : Lean.Level → Bool
-- Lean.Elab.InfoTree.Types
Lean.Elab.MacroExpansionInfo.stx : Lean.Elab.MacroExpansionInfo → Lean.Syntax
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.constantsToVars.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_4} {γ : Type u_2} (motive : (L.withConstants γ).Term α → Sort u_5) (_n : ℕ)
  (f : (L.withConstants γ).Functions (_n + 1)) (ts : Fin (_n + 1) → (L.withConstants γ).Term α)
  (h_1 : (a : α) → motive (FirstOrder.Language.var a))
  (h_2 :
    (f : (L.withConstants γ).Functions 0) →
      (ts : Fin 0 → (L.withConstants γ).Term α) → motive (FirstOrder.Language.func f ts))
  (h_3 :
    (_n : ℕ) →
      (f : (L.withConstants γ).Functions (_n + 1)) →
        (ts : Fin (_n + 1) → (L.withConstants γ).Term α) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.func f ts with
    | FirstOrder.Language.var a => h_1 a
    | FirstOrder.Language.func f ts => h_2 f ts
    | FirstOrder.Language.func f ts => h_3 _n f ts) =
    h_3 _n f ts
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- Constructor for morphisms to `(t.truncLE n).obj Y`.  -/
CategoryTheory.Triangulated.TStructure.liftTruncLE : {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 : ℤ) → [t.IsLE X n] → X ⟶ (t.truncLE n).obj Y
-- Mathlib.Combinatorics.Graph.Simple
Graph.ofSimpleGraph_adj_iff : ∀ {α : Type u_1} {G : SimpleGraph α} (u v : α), (Graph.ofSimpleGraph G).Adj u v ↔ G.Adj u v
-- Lean.Parser.Tactic.Doc
/-- The mapping between tags and tactics. Tags may be applied in any module, not just the defining
module for the tactic.

Because this is expected to be augmented regularly, but queried rarely (only when generating
documentation indices), it is just stored as flat unsorted arrays of pairs. Before it is used for
some other purpose, consider a new representation.

The first projection in each pair is the tactic name, and the second is the tag name.
 -/
Lean.Parser.Tactic.Doc.tacticTagExt : Lean.PersistentEnvExtension (Lean.Name × Lean.Name) (Lean.Name × Lean.Name) (Lean.NameMap Lean.NameSet)
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Icc_of_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ico b a → x ∈ Set.Icc b a
-- Mathlib.SetTheory.Cardinal.Free
instInfiniteFreeMonoidOfNonempty : ∀ (α : Type u) [Nonempty α], Infinite (FreeMonoid α)
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β},
  s.IsPWO → t.IsPWO → (s ×ˢ t).IsPWO
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_mul : ∀ {R : Type u} [inst : CommSemiring R] (I J : Ideal R),
  PrimeSpectrum.zeroLocus ↑(I * J) = PrimeSpectrum.zeroLocus ↑I ∪ PrimeSpectrum.zeroLocus ↑J
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is induced map `Z¹(H, A) ⟶ Z¹(G, B)`.  -/
groupCohomology.mapCocycles₁ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{max u u_1, u, u} k H} →
          {B : Rep.{max u u_1, u, u} k G} →
            (f : G →* H) →
              (Rep.res f A ⟶ B) →
                (ModuleCat.of k ↥(groupCohomology.cocycles₁ A) ⟶ ModuleCat.of k ↥(groupCohomology.cocycles₁ B))
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- More flexible variant of `mapComp`. (See `Bicategory.Functor.Strict`
for applications to strict bicategories.)  -/
CategoryTheory.Pseudofunctor.mapComp' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.Pseudofunctor B C) →
          {b₀ b₁ b₂ : B} →
            (f : b₀ ⟶ b₁) →
              (g : b₁ ⟶ b₂) →
                (fg : b₀ ⟶ b₂) →
                  autoParam (CategoryTheory.CategoryStruct.comp f g = fg)
                      CategoryTheory.Pseudofunctor.mapComp'._auto_1 →
                    (F.map fg ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g))
-- Mathlib.Topology.ExtremallyDisconnected
_private.Mathlib.Topology.ExtremallyDisconnected.0.ExtremallyDisconnected.homeoCompactToT2_injective : ∀ {A E : Type u} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace E] [ExtremallyDisconnected A] [T2Space A]
  [T2Space E] [CompactSpace E] {ρ : E → A},
  Continuous ρ →
    Function.Surjective ρ → (∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed E₀ → ρ '' E₀ ≠ Set.univ) → Function.Injective ρ
-- Std.Async.Select
Std.Async.Selector.mk : {α : Type} →
  Std.Async.Async (Option α) → (Std.Async.Waiter α → Std.Async.Async Unit) → Std.Async.Async Unit → Std.Async.Selector α
-- Lean.Data.Lsp.Client
Lean.Lsp.instFromJsonRegistration.fromJson : Lean.Json → Except String Lean.Lsp.Registration
-- Mathlib.Topology.Order.Basic
/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
hold eventually for the filter.  -/
tendsto_of_tendsto_of_tendsto_of_le_of_le' : ∀ {α : Type u} {β : Type v} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {f g h : β → α}
  {b : Filter β} {a : α},
  Filter.Tendsto g b (nhds a) →
    Filter.Tendsto h b (nhds a) →
      (∀ᶠ (b : β) in b, g b ≤ f b) → (∀ᶠ (b : β) in b, f b ≤ h b) → Filter.Tendsto f b (nhds a)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
isCountablySpanning_measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α], IsCountablySpanning {s | MeasurableSet s}
-- Mathlib.RingTheory.Localization.Submodule
IsFractionRing.coeSubmodule_isPrincipal : ∀ (R : Type u_3) (K : Type u_4) [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I : Ideal R}, (IsLocalization.coeSubmodule K I).IsPrincipal ↔ Submodule.IsPrincipal I
-- Mathlib.NumberTheory.ModularForms.LFunction
/-- For cusp forms the FE-pair is a strong FE-pair.  -/
CuspForm.isStrongFEPair : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) [inst_2 : CuspFormClass F Γ k],
  IsStrongFEPair (ModularForm.weakFEPair hk f)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even.algHom_ext_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A]
  {f g : ↥(CliffordAlgebra.even Q) →ₐ[R] A},
  f = g ↔ (CliffordAlgebra.even.ι Q).compr₂ f = (CliffordAlgebra.even.ι Q).compr₂ g
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- A finite-dimensional subspace is complete.  -/
Submodule.complete_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : UniformSpace E] [T2Space E] [IsUniformAddGroup E] [inst_6 : Module 𝕜 E] [ContinuousSMul 𝕜 E]
  (s : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥s], IsComplete ↑s
-- Mathlib.Algebra.Group.Graph
/-- **Vertical line test** for additive monoid homomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that `G` surjects onto the first
factor and `G` intersects every "vertical line" `{(h, i) | i : I}` at most once. Then `G` is the
graph of some monoid homomorphism `f : H → I`.  -/
AddSubmonoid.exists_eq_mgraph : ∀ {H : Type u_2} {I : Type u_3} [inst : AddMonoid H] [inst_1 : AddMonoid I] {G : AddSubmonoid (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → ∃ f, G = f.mgraph
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.extendScalars_algebra₁ : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), P.extendScalars.algebra₁ = Algebra.id P.Ring
-- Mathlib.Order.Monotone.Monovary
monovaryOn_self : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder α] (f : ι → α) (s : Set ι), MonovaryOn f f s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Let `C(G, A)` denote the complex of inhomogeneous cochains of `A : Rep k G`. This lemma
says `d₁₂` gives a simpler expression for the 1st differential: that is, the following
square commutes:
```
  C¹(G, A) ---d 1 2---> C²(G, A)
    |                      |
    |                      |
    |                      |
    v                      v
  Fun(G, A) --d₁₂--> Fun(G × G, A)
```
where the vertical arrows are `cochainsIso₁` and `cochainsIso₂` respectively.
 -/
groupCohomology.comp_d₁₂_eq : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).hom (groupCohomology.d₁₂ A) =
    CategoryTheory.CategoryStruct.comp ((groupCohomology.inhomogeneousCochains A).d 1 2)
      (groupCohomology.cochainsIso₂ A).hom
-- Lean.Data.Lsp.Communication
/-- Returns the Content-Length.  -/
_private.Lean.Data.Lsp.Communication.0.Lean.IO.FS.Stream.readLspHeader : IO.FS.Stream → IO ℕ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.homEquiv_chgUniv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] [inst_3 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ}
  [inst_4 : HasDerivedCategory C] (e : CategoryTheory.Abelian.Ext X Y n),
  CategoryTheory.Abelian.Ext.homEquiv (CategoryTheory.Abelian.Ext.chgUniv e) = CategoryTheory.Abelian.Ext.homEquiv e
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_eq_sum : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F),
  (Lagrange.interpolate s v) r =
    ∑ i ∈ s, Polynomial.C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∏ j ∈ s.erase i, (Polynomial.X - Polynomial.C (v j))
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- `X.CanonicallyOverClass S` is the typeclass containing the data of a
structure morphism `X ↘ S : X ⟶ S`,
and that `S` is (uniquely) inferable from the structure of `X`.
 -/
CategoryTheory.CanonicallyOverClass : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → semiOutParam C → Type v
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Poly.gcdCoeffs.go : Lean.Grind.CommRing.Poly → ℕ → ℕ
-- Init.Data.Array.Erase
_private.Init.Data.Array.Erase.0.List.eraseP_filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (y : β) → motive (some y)) (h_2 : Unit → motive none),
  (match none with
    | some y => h_1 y
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce.churchRosser.eq_1 : ∀ {α : Type u_1} {L₁ L₂ L₃ : List (α × Bool)} [inst : DecidableEq α] (H12 : FreeAddGroup.Red L₁ L₂)
  (H13 : FreeAddGroup.Red L₁ L₃), FreeAddGroup.reduce.churchRosser H12 H13 = ⟨FreeAddGroup.reduce L₁, ⋯⟩
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.toOuterMeasure_bind_apply : ∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (s : Set β),
  (p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- For any infinite place `w'`, the regulator of the family `u` is equal to the absolute value of
the determinant of the matrix with entries `(mult w * log w (u i))_i` for `w ≠ w'`.
 -/
NumberField.Units.regOfFamily_eq_det : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) (w' : NumberField.InfinitePlace K)
  (e : { w // w ≠ w' } ≃ Fin (NumberField.Units.rank K)),
  NumberField.Units.regOfFamily u =
    |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(u (e i))))).det|
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic on `U`, if `g` agrees with `f` on a codiscrete subset of `U` and outside of
`U`, then `g` is also meromorphic on `U`.
 -/
MeromorphicOn.congr_codiscreteWithin_of_eqOn_compl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → f =ᶠ[Filter.codiscreteWithin U] g → Set.EqOn f g Uᶜ → MeromorphicOn g U
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.toReal_gaussianPDF : ∀ {μ : ℝ} {v : NNReal} (x : ℝ), (ProbabilityTheory.gaussianPDF μ v x).toReal = ProbabilityTheory.gaussianPDFReal μ v x