mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.whiskerLeft_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C) {Y₁ Y₂ : CategoryTheory.Center C} (f : Y₁ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.fst f.f
-- Mathlib.Data.List.OffDiag
/-- `List.offDiag l` has no duplicates iff the original list has no duplicates.  -/
List.nodup_offDiag : ∀ {α : Type u_1} {l : List α}, l.offDiag.Nodup ↔ l.Nodup
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.instFinite : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] [inst_1 : Std.IteratorAccess α m]
  [inst_2 : Monad m] [Std.Iterators.Finite α m], Std.Iterators.Finite (Std.Iterators.Types.StepSizeIterator α m β) m
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.ofSign_disjUnion : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α],
  (Equiv.Perm.ofSign 1).disjUnion (Equiv.Perm.ofSign (-1)) ⋯ = Finset.univ
-- Mathlib.Data.EReal.Basic
instNontrivialEReal : Nontrivial EReal
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.negRev_append : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)},
  FreeAddGroup.negRev (L₁ ++ L₂) = FreeAddGroup.negRev L₂ ++ FreeAddGroup.negRev L₁
-- Mathlib.Algebra.Group.Hom.Defs
/-- Copy of a `OneHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
OneHom.copy : {M : Type u_4} →
  {N : Type u_5} → [inst : One M] → [inst_1 : One N] → (f : OneHom M N) → (f' : M → N) → f' = ⇑f → OneHom M N
-- Mathlib.Order.CompleteBooleanAlgebra
iInf_codisjoint_iff : ∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] {a : α} {f : ι → α},
  Codisjoint (⨅ i, f i) a ↔ ∀ (i : ι), Codisjoint (f i) a
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.mem_lowerCentralSeries_succ_iff : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G) (n : ℕ) (q : G),
  q ∈ S.lowerCentralSeries (n + 1) ↔ q ∈ AddSubgroup.closure {x | ∃ p ∈ S.lowerCentralSeries n, ∃ q ∈ S, ⁅p, q⁆ = x}
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β),
  ↑(MeasureTheory.AEEqFun.comp g hg f) =ᵐ[μ] g ∘ ↑f
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.check : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Order.RelIso.Basic
/-- To define a relation embedding from an antisymmetric relation `r` to a reflexive relation `s`
it suffices to give a function together with a proof that it satisfies `s (f a) (f b) ↔ r a b`.
 -/
RelEmbedding.ofMapRelIff : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      {s : β → β → Prop} → (f : α → β) → [Std.Antisymm r] → [Std.Refl s] → (∀ (a b : α), s (f a) (f b) ↔ r a b) → r ↪r s
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Complex.Gammaℝ_one : Complex.Gammaℝ 1 = 1
-- Mathlib.Algebra.Category.CommBialgCat
/-- The underlying bialgebra map.  -/
CommBialgCat.Hom.hom' : {R : Type u} → [inst : CommRing R] → {A B : CommBialgCat R} → A.Hom B → ↑A →ₐc[R] ↑B
-- Mathlib.Probability.Density
MeasureTheory.pdf.congr : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {X Y : Ω → E}, X =ᵐ[ℙ] Y → MeasureTheory.pdf X ℙ μ = MeasureTheory.pdf Y ℙ μ
-- Mathlib.Data.Finsupp.MonomialOrder
/-- Given a monomial order, notation for the corresponding order relation on `σ →₀ ℕ`  -/
MonomialOrder.«term_≼[_]_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.Scheme.Hom.finrank_eq_finrank_snd_of_isAffine : ∀ {X S T : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : T ⟶ S) [inst : AlgebraicGeometry.IsAffine T] (t : ↥T)
  [AlgebraicGeometry.Flat f] [AlgebraicGeometry.IsFinite f],
  AlgebraicGeometry.Scheme.Hom.finrank f (g t) =
    AlgebraicGeometry.IsAffine.finrank✝ (CategoryTheory.Limits.pullback.snd f g) t
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_le_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] (x : ↑(Set.Icc 0 1)), ↑x ≤ 1
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_opow_omega0`. -/
Ordinal.principal_opow_omega0 : Ordinal.IsPrincipal (fun x1 x2 => x1 ^ x2) Ordinal.omega0
-- Mathlib.Control.Monad.Cont
/-- Note that `tryCatch` does not have correct behavior in this monad:
```
def foo : ContT Bool (Except String) Bool := do
  let x ← try
    pure true
  catch _ =>
    return false
  throw s!"oh no {x}"
#eval foo.run pure
-- `Except.ok false`, no error
```
Here, the `throwError` is being run inside the `try`.
See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/MonadExcept.20in.20the.20ContT.20monad/near/375341221)
for further discussion.
 -/
ContT.instMonadExceptOf : {r : Type u} → {m : Type u → Type v} → (ε : Type u_1) → [MonadExceptOf ε m] → MonadExceptOf ε (ContT r m)
-- Mathlib.Topology.DiscreteQuotient
/-- `finsetClopens X` is injective.  -/
DiscreteQuotient.finsetClopens_inj : ∀ (X : Type u_2) [inst : TopologicalSpace X] [inst_1 : CompactSpace X],
  Function.Injective (DiscreteQuotient.finsetClopens X)
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasDerivAt_iff_isLittleO`. -/
HasDerivAt.isLittleO : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x → (fun x' => f x' - f x - (x' - x) • f') =o[nhds x] fun x' => x' - x
-- Mathlib.SetTheory.ZFC.PSet
PSet.mk_func : ∀ (α : Type u_1) (A : α → PSet.{u_1}), (PSet.mk α A).Func = A
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftIso_inv_naturality : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y : C} (n a a' : M) (ha' : n + a = a')
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.shift a').map f) ((F.shiftIso n a a' ha').inv.app Y) =
    CategoryTheory.CategoryStruct.comp ((F.shiftIso n a a' ha').inv.app X)
      ((F.shift a).map ((CategoryTheory.shiftFunctor C n).map f))
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instZero : (R : Type u_1) → (X : Type u_2) → [inst : CommSemiring R] → Zero (FreeAlgebra R X)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_assemble₃Unchecked : ∀ {w x y : UInt8},
  (ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y).toBitVec =
    BitVec.setWidth 32 (BitVec.setWidth 4 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec ++ BitVec.setWidth 6 y.toBitVec)
-- Init.Data.Array.Find
Array.findSome?_replicate_of_pos : ∀ {n : ℕ} {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α},
  0 < n → Array.findSome? f (Array.replicate n a) = f a
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_counitIso_inv_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor (C × D) E) (X_1 : C × D),
  (CategoryTheory.Functor.currying.counitIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (X_1.1, X_1.2))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.Trimmed.nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)} {f : ℝ → ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
      f).Trimmed
-- Std.Data.TreeMap.Raw.DecidableEquiv
Std.TreeMap.Raw.instDecidableEquiv : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] →
          [inst : BEq β] → [LawfulBEq β] → {t₁ t₂ : Std.TreeMap.Raw α β cmp} → t₁.WF → t₂.WF → Decidable (t₁.Equiv t₂)
-- Mathlib.Algebra.Order.Hom.Basic
AddGroupNormClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : AddGroup α] [inst_1 : AddCommMonoid β]
  [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [toAddGroupSeminormClass : AddGroupSeminormClass F α β],
  (∀ (f : F) {a : α}, f a = 0 → a = 0) → AddGroupNormClass F α β
-- Mathlib.Order.Sublattice
Sublattice.prodEquiv_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L : Sublattice α) (M : Sublattice β)
  (x : { c // (fun x => x ∈ ↑L) c.1 ∧ (fun x => x ∈ ↑M) c.2 }), (L.prodEquiv M) x = (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩)
-- Mathlib.GroupTheory.Sylow
Sylow.mulAction : {p : ℕ} → {G : Type u_1} → [inst : Group G] → MulAction G (Sylow p G)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The constant `MulticospanShape` for a pair of parallel morphisms.  -/
CategoryTheory.Limits.MulticospanIndex.ofParallelHoms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.Limits.MulticospanShape) →
      {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → CategoryTheory.Limits.MulticospanIndex J C
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `mem_segment_iff_wbtw`. -/
Wbtw.mem_segment : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [IsOrderedRing R] {x y z : V}, Wbtw R x y z → y ∈ segment R x z
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.push.injEq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Γ k) (a_1 : Turing.TM2.Stmt Γ Λ σ)
  (k_1 : K) (a_2 : σ → Γ k_1) (a_3 : Turing.TM2.Stmt Γ Λ σ),
  (Turing.TM2.Stmt.push k a a_1 = Turing.TM2.Stmt.push k_1 a_2 a_3) = (k = k_1 ∧ a ≍ a_2 ∧ a_1 = a_3)
-- Mathlib.CategoryTheory.Sites.MorphismProperty
/-- If `P` is a multiplicative morphism property which is stable under base change on a category
`C` with pullbacks, then `P` induces a pretopology, where coverings are given by presieves whose
elements satisfy `P`.  -/
CategoryTheory.MorphismProperty.pretopology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      (P : CategoryTheory.MorphismProperty C) →
        [P.IsMultiplicative] → [P.IsStableUnderBaseChange] → CategoryTheory.Pretopology C
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.clift_apply_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : FreeAddMonoid (M ⊕ N) →+ P) (hM₁ : f (FreeAddMonoid.of (Sum.inl 0)) = 0)
  (hN₁ : f (FreeAddMonoid.of (Sum.inr 0)) = 0)
  (hM :
    ∀ (x y : M),
      f (FreeAddMonoid.of (Sum.inl (x + y))) = f (FreeAddMonoid.of (Sum.inl x) + FreeAddMonoid.of (Sum.inl y)))
  (hN :
    ∀ (x y : N),
      f (FreeAddMonoid.of (Sum.inr (x + y))) = f (FreeAddMonoid.of (Sum.inr x) + FreeAddMonoid.of (Sum.inr y)))
  (x : N), (AddMonoid.Coprod.clift f hM₁ hN₁ hM hN) (AddMonoid.Coprod.inr x) = f (FreeAddMonoid.of (Sum.inr x))
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_rci : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, (Std.Rci.Sliceable.mkSlice xs lo...*).stop = xs.size
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.smul_apply : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : MulAction G β] (g : G) (f : α ↪ β) (a : α),
  (g • f) a = g • f a
-- Aesop.Forward.State
/-- States for each of the rule's slot clusters.  -/
Aesop.RuleState.clusterStates : Aesop.RuleState → Array Aesop.ClusterState
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the first vector passed to `oangle` is 0, the result is 0.  -/
Orientation.oangle_zero_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), o.oangle 0 x = 0
-- Init.Data.String.Search
/-- Returns the last character in `s`. If `s = ""`, returns `(default : Char)`.

Examples:

* `"abc".back = 'c'`

* `"".back = (default : Char)`
 -/
String.back : String → Char
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.expMap = NumberField.mixedEmbedding.fundamentalCone.expMap
-- Mathlib.Data.Set.Function
Set.injOn_pair : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a b : α}, Set.InjOn f {a, b} ↔ f a = f b → a = b
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β) (f' : α → β)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
Continuous.integrableOn_uIoc : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_5 : LinearOrder X] [CompactIccSpace X] [T2Space X],
  Continuous f → MeasureTheory.IntegrableOn f (Set.uIoc a b) μ
-- Std.Data.TreeSet.Basic
/-- Returns `true` if `a`, or an element equal to `a` according to the comparator `cmp`, is contained
in the set. There is also a `Prop`-valued version of this: `a ∈ t` is equivalent to
`t.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for equality checks, while for tree sets, both use the given comparator `cmp`.
 -/
Std.TreeSet.contains : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.of_forall_get?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → (∀ (k : α), t₁.get? k = t₂.get? k) → t₁.Equiv t₂
-- Mathlib.Analysis.Convex.Basic
Convex.add_smul_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E} [AddRightMono 𝕜],
  Convex 𝕜 s → ∀ {x y : E}, x ∈ s → x + y ∈ s → ∀ {t : 𝕜}, t ∈ Set.Icc 0 1 → x + t • y ∈ s
-- Lean.CoreM
Lean.Core.instMonadLiftIOCoreM : MonadLift IO Lean.CoreM
-- Mathlib.Tactic.Widget.Calc
/-- Code action to create a `calc` tactic from the current goal.  -/
createCalc : Batteries.CodeAction.TacticCodeAction
-- Mathlib.Data.ENat.Basic
ENat.map_natCast_injective : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α],
  Function.Injective (ENat.map Nat.cast)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_add_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] (a b : α), {a} + {b} = {a + b}
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f g : M [⋀^ι]→L[R] N) [inst_7 : ContinuousAdd N], ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.setIntegral_norm_condExp_rpow_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {p : ℝ},
  1 ≤ p →
    ∀ {f : α → E} {s : Set α},
      MeasurableSet s →
        MeasureTheory.Integrable (fun x => ‖f x‖ ^ p) μ →
          ∫ (x : α) in s, ‖μ[f | m] x‖ ^ p ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ^ p ∂μ
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.tendsto_lintegral_norm_of_dominated_convergence : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {F : ℕ → α → β} {f : α → β} {bound : α → ℝ},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ) →
    MeasureTheory.HasFiniteIntegral bound μ →
      (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
          Filter.Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) Filter.atTop (nhds 0)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.mk : Lean.Syntax.Traverser →
  Option ℕ → Lean.Name → Option ℕ → Option ℕ → Lean.Name → Bool → Lean.PrettyPrinter.Parenthesizer.State
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.instEssSurjIncl : FintypeCat.Skeleton.incl.EssSurj
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_mem_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α} {a : α}, a⁻¹ ∈ s⁻¹ ↔ a ∈ s
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instVAddAssocClass_1 : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X],
  VAddAssocClass R (AddOreLocalization S M) (AddOreLocalization S X)
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.HasCardinalFilteredGenerator.exists_generator : ∀ (C : Type u) [hC : CategoryTheory.Category.{v, u} C] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular]
  [self : CategoryTheory.HasCardinalFilteredGenerator C κ],
  ∃ P, ∃ (_ : CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P), P.IsCardinalFilteredGenerator κ
-- Mathlib.Algebra.Order.Floor.Defs
Nat.lt_ceil : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a : α} {n : ℕ},
  n < ⌈a⌉₊ ↔ ↑n < a
-- Mathlib.GroupTheory.Perm.Cycle.Type
List.Vector.replicate.eq_1 : ∀ {α : Type u_1} (n : ℕ) (a : α), List.Vector.replicate n a = ⟨List.replicate n a, ⋯⟩
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_uniformity_ofCore_iff : ∀ {α : Type ua} {u : UniformSpace.Core α} {s : SetRel α α}, s ∈ uniformity α ↔ s ∈ u.uniformity
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Inhabited α] {k k' : α} {f : β → β},
  (Std.DTreeMap.Const.modify t k f).getKey! k' =
    if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.monoidOf.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M),
  Localization.monoidOf S = { toFun := fun x => Localization.mk x 1, map_mul' := ⋯, isLocalizationMap := ⋯ }
-- Mathlib.Data.Num.Basic
PosNum.bit1 : PosNum → PosNum
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The equivalence between finite places and maximal ideals.  -/
NumberField.FinitePlace.equivHeightOneSpectrum : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      NumberField.FinitePlace K ≃ IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.conjTranspose_mul_self_mul_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {p : Type u_5}
  (A : Matrix m n R) (B : Matrix n p R), A.conjTranspose * A * B = 0 ↔ A * B = 0
-- Init.Core
String.ofByteArray.injEq : ∀ (toByteArray : ByteArray) (isValidUTF8 : toByteArray.IsValidUTF8) (toByteArray_1 : ByteArray)
  (isValidUTF8_1 : toByteArray_1.IsValidUTF8),
  ({ toByteArray := toByteArray, isValidUTF8 := isValidUTF8 } =
      { toByteArray := toByteArray_1, isValidUTF8 := isValidUTF8_1 }) =
    (toByteArray = toByteArray_1)
-- Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
/-- For `C` closed monoidal, build an instance of `C` as a `C`-category  -/
CategoryTheory.MonoidalClosed.enrichedCategorySelf : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.MonoidalClosed C] → CategoryTheory.EnrichedCategory C C
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_map : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B]
  (S : NonUnitalStarSubalgebra R A) (f : F), ↑(NonUnitalStarSubalgebra.map f S) = ⇑f '' ↑S
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk'_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y' Y'' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right ⟶ Y')
  (g' : Y' ⟶ Y''),
  f.homMk' (CategoryTheory.CategoryStruct.comp g g') =
    CategoryTheory.CategoryStruct.comp (f.homMk' g)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp f.hom (T.map g))).homMk' g')
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.equiv_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {E' : Type u_7} [inst_4 : Fintype ι']
  [inst_5 : NormedAddCommGroup E'] [inst_6 : InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E)
  (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') (x : E), (b.equiv b' e) x = ∑ i, (b.repr x).ofLp i • b' (e i)
-- Mathlib.Order.Disjoint
IsCompl.of_eq : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x y : α}, x ⊓ y = ⊥ → x ⊔ y = ⊤ → IsCompl x y
-- Mathlib.Analysis.InnerProductSpace.Adjoint
InnerProductSpace.isStarProjection_rankOne_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {x : E}, ‖x‖ = 1 → IsStarProjection (((InnerProductSpace.rankOne 𝕜) x) x)
-- Mathlib.Combinatorics.Matroid.Basic
/-- `Matroid.IsBasis' I X` is the same as `Matroid.IsBasis I X`,
without the requirement that `X ⊆ M.E`. This is convenient for some
API building, especially when working with rank and closure.  -/
Matroid.IsBasis' : {α : Type u_1} → Matroid α → Set α → Set α → Prop
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrLeft_apply : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : AddZeroClass M₁] [inst_1 : AddZeroClass M₂]
  [inst_2 : AddCommMonoid N] (e : M₁ ≃+ M₂) (f : M₁ →+ N), e.addMonoidHomCongrLeft f = f.comp ↑e.symm
-- Mathlib.Analysis.Calculus.Gradient.Basic
inner_gradient_right : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x y : F}, inner 𝕜 x (gradient f y) = (starRingEnd 𝕜) ((fderiv 𝕜 f y) x)
-- Std.Http.Protocol.H1.Writer
/-- Checks if the connection should be kept alive based on the Connection header.
 -/
Std.Http.Protocol.H1.Writer.shouldKeepAlive : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Bool
-- Mathlib.Algebra.Polynomial.Coeff
/-- The nth coefficient, as a linear map.  -/
Polynomial.lcoeff : (R : Type u) → [inst : Semiring R] → ℕ → Polynomial R →ₗ[R] R
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.subset_ground : ∀ {α : Type u_2} (self : IndepMatroid α) (I : Set α), self.Indep I → I ⊆ self.E