mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Whiskering a right exact functor by a right exact functor yields a right exact functor.  -/
CategoryTheory.RightExactFunctor.whiskeringRight : (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] →
            CategoryTheory.Functor (D ⥤ᵣ E) (CategoryTheory.Functor (C ⥤ᵣ D) (C ⥤ᵣ E))
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instContinuousEvalConst : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R], ContinuousEvalConst (ContinuousMapZero X R) X R
-- Mathlib.Algebra.Regular.Prod
IsRegular.prodMk : ∀ {R : Type u_2} {S : Type u_3} [inst : Mul R] [inst_1 : Mul S] {a : R} {b : S},
  IsRegular a → IsRegular b → IsRegular (a, b)
-- Mathlib.Data.List.Rotate
List.length_rotate' : ∀ {α : Type u} (l : List α) (n : ℕ), (l.rotate' n).length = l.length
-- Mathlib.Analysis.Seminorm
Seminorm.instIsAddApplyReal : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E],
  IsAddApply (Seminorm 𝕜 E) E ℝ
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.IsGroupoid.all_isIso : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsGroupoid C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by applying the div operation.
 -/
Std.Time.Internal.Bounded.LE.ediv : {n m : ℤ} → Std.Time.Internal.Bounded.LE n m → (num : ℤ) → num > 0 → Std.Time.Internal.Bounded.LE (n / num) (m / num)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.FirstObj.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))} {X : C}
  {R : CategoryTheory.Presieve X} {z₁ z₂ : CategoryTheory.Equalizer.FirstObj P R},
  z₁ = z₂ ↔
    ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
      (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩))
          z₁ =
        (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) ⟨Y, ⟨f, hf⟩⟩))
          z₂
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The isomorphism which an adjunction `F ⊣ G` induces on `G ⋙ yoneda`. This states that
`Adjunction.homEquiv` is natural in both arguments.  -/
CategoryTheory.Adjunction.compYonedaIso : {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} →
            (F ⊣ G) →
              (G.comp CategoryTheory.yoneda ≅
                CategoryTheory.yoneda.comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op))
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- Build a `QuadraticForm.IsometryEquiv` from an isomorphism in the category
`QuadraticModuleCat R`.  -/
CategoryTheory.Iso.toIsometryEquiv : {R : Type u} → [inst : CommRing R] → {X Y : QuadraticModuleCat R} → (X ≅ Y) → QuadraticMap.IsometryEquiv X.form Y.form
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- See Note [custom simps projection].  -/
QuadraticMap.Isometry.Simps.apply : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} → {Q₂ : QuadraticMap R M₂ N} → (Q₁ →qᵢ Q₂) → M₁ → M₂
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map,
and `j : M →+ M'` is an injective monoid map, such that the scalar multiplications
on `M` and `M'` are compatible, then `j` sends linearly independent families
of vectors to linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map_injOn`.
TODO : `LinearIndepOn` version.  -/
LinearIndependent.map_of_surjective_injectiveₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {R' : Type u_6} {M' : Type u_7} [inst_3 : Semiring R'] [inst_4 : AddCommMonoid M']
  [inst_5 : Module R' M'],
  LinearIndependent R v →
    ∀ (i : R → R') (j : M →+ M'),
      Function.Surjective i →
        Function.Injective ⇑j → (∀ (r : R) (m : M), j (r • m) = i r • j m) → LinearIndependent R' (⇑j ∘ v)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixingSubgroup_bot : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [SMulCommClass G K L], fixingSubgroup G ↑⊥ = ⊤
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_update : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R) (x : MonoidAlgebra R M),
  (MonoidAlgebra.update m r x).coeff = x.coeff.update m r
-- Mathlib.Order.SymmDiff
bihimp_top : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a : α), bihimp a ⊤ = a
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful),
  F.ReflectsIsomorphisms
-- Mathlib.GroupTheory.Congruence.Defs
/-- The morphism into the quotient by an additive congruence relation  -/
AddCon.toQuotient : {M : Type u_1} → [inst : Add M] → {c : AddCon M} → M → c.Quotient
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_le_of_sum_range_le : ∀ {f : ℕ → ENNReal} {c : ENNReal}, (∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) → ∑' (n : ℕ), f n ≤ c
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- An isomorphism of `1`-hypercovers is an isomorphism of pre-`1`-hypercovers.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {S : C} → {E F : J.OneHypercover S} → (E.toPreOneHypercover ≅ F.toPreOneHypercover) → (E ≅ F)
-- Init.RCases
/-- `rcases` is a tactic that will perform `cases` recursively, according to a pattern. It is used to
destructure hypotheses or expressions composed of inductive types like `h1 : a ∧ b ∧ c ∨ d` or
`h2 : ∃ x y, trans_rel R x y`. Usual usage might be `rcases h1 with ⟨ha, hb, hc⟩ | hd` or
`rcases h2 with ⟨x, y, _ | ⟨z, hxz, hzy⟩⟩` for these examples.

Each element of an `rcases` pattern is matched against a particular local hypothesis (most of which
are generated during the execution of `rcases` and represent individual elements destructured from
the input expression). An `rcases` pattern has the following grammar:

* A name like `x`, which names the active hypothesis as `x`.
* A blank `_`, which does nothing (letting the automatic naming system used by `cases` name the
  hypothesis).
* A hyphen `-`, which clears the active hypothesis and any dependents.
* The keyword `rfl`, which expects the hypothesis to be `h : a = b`, and calls `subst` on the
  hypothesis (which has the effect of replacing `b` with `a` everywhere or vice versa).
* A type ascription `p : ty`, which sets the type of the hypothesis to `ty` and then matches it
  against `p`. (Of course, `ty` must unify with the actual type of `h` for this to work.)
* A tuple pattern `⟨p1, p2, p3⟩`, which matches a constructor with many arguments, or a series
  of nested conjunctions or existentials. For example if the active hypothesis is `a ∧ b ∧ c`,
  then the conjunction will be destructured, and `p1` will be matched against `a`, `p2` against `b`
  and so on.
* A `@` before a tuple pattern as in `@⟨p1, p2, p3⟩` will bind all arguments in the constructor,
  while leaving the `@` off will only use the patterns on the explicit arguments.
* An alternation pattern `p1 | p2 | p3`, which matches an inductive type with multiple constructors,
  or a nested disjunction like `a ∨ b ∨ c`.

A pattern like `⟨a, b, c⟩ | ⟨d, e⟩` will do a split over the inductive datatype,
naming the first three parameters of the first constructor as `a,b,c` and the
first two of the second constructor `d,e`. If the list is not as long as the
number of arguments to the constructor or the number of constructors, the
remaining variables will be automatically named. If there are nested brackets
such as `⟨⟨a⟩, b | c⟩ | d` then these will cause more case splits as necessary.
If there are too many arguments, such as `⟨a, b, c⟩` for splitting on
`∃ x, ∃ y, p x`, then it will be treated as `⟨a, ⟨b, c⟩⟩`, splitting the last
parameter as necessary.

`rcases` also has special support for quotient types: quotient induction into Prop works like
matching on the constructor `quot.mk`.

`rcases h : e with PAT` will do the same as `rcases e with PAT` with the exception that an
assumption `h : e = PAT` will be added to the context.
 -/
Lean.Parser.Tactic.rcases : Lean.ParserDescr
-- Mathlib.Algebra.Category.Semigrp.Basic
_private.Mathlib.Algebra.Category.Semigrp.Basic.0.MagmaCat.Hom.mk.injEq : ∀ {A B : MagmaCat} (hom' hom'_1 : ↑A →ₙ* ↑B), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_6 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (n : ℕ),
  x = Lean.Grind.CommRing.Expr.natCast n →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_6 n
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equiv_inv_hom_apply_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : (X : Cᵒᵖ) × ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).inv) c).π = c.snd
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.instTrans : {α : Type u} → {cmp : α → α → Ordering} → Trans Std.TreeSet.Raw.Equiv Std.TreeSet.Raw.Equiv Std.TreeSet.Raw.Equiv
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofNatClamp_of_lt : ∀ {n : ℕ} (hn : n < USize.size), (USize.ofNatClamp n).toBitVec = n#'hn
-- Mathlib.RingTheory.Bialgebra.Basic
/-- The counit on a bialgebra preserves 1.  -/
Bialgebra.counit_one : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : Bialgebra R A],
  CoalgebraStruct.counit 1 = 1
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.instStrongNormalizedGCDMonoid : {R : Type u_1} → [inst : CommRing R] → [StrongNormalizedGCDMonoid R] → StrongNormalizedGCDMonoid (Polynomial R)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.toUpper_ofUpper : ∀ {α : Type u_1} (a : Topology.WithUpper α), Topology.WithUpper.toUpper (Topology.WithUpper.ofUpper a) = a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.mk_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g),
  (CategoryTheory.Limits.PullbackCone.mk fst snd eq).snd = snd
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.OplaxLeftLinear C] (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) d)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso (F.obj d)).hom =
    F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.mul_add : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {o : Type u_7} [inst : Fintype n] [inst_1 : NonUnitalNonAssocSemiring A]
  (L : CStarMatrix m n A) (M N : CStarMatrix n o A), L * (M + N) = L * M + L * N
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.isNormal_preAleph : Order.IsNormal ⇑Cardinal.preAleph
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_alterKey_eq_self' : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  Std.Internal.List.containsKey k l = false →
    (f (Std.Internal.List.getValue? k l)).isNone = true → (Std.Internal.List.Const.alterKey k f l).length = l.length
-- Mathlib.Data.Setoid.Basic
/-- The infimum of two equivalence relations.  -/
Setoid.instMin_mathlib : {α : Type u_1} → Min (Setoid α)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.mk.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (as : C), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- Given two family of morphisms `f : X i ⟶ S` and `f' : X' j ⟶ S`,
two objects `D₁ D₂ : F.DescentData f`, a morphism `φ` between the images in
`F.DescentData f'` of `D₁` and `D₂` by a functor `pullFunctor`, and a factorization
`a ≫ f' j = q ≫ f i`, this is the section on `Over.mk q` of the presheaf
of morphisms from `D₁.obj i` to `D₂.obj i` that is obtained by pulling back `φ.hom j`.  -/
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor : {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} →
              {ι' : Type t'} →
                {X' : ι' → C} →
                  {f' : (j : ι') → X' j ⟶ S} →
                    {α : ι' → ι} →
                      {p' : (j : ι') → X' j ⟶ X (α j)} →
                        (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j) →
                          {D₁ D₂ : F.DescentData f} →
                            ((CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
                                (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂) →
                              ⦃i : ι⦄ →
                                {Z : C} →
                                  (q : Z ⟶ X i) →
                                    ⦃j : ι'⦄ →
                                      (a : Z ⟶ X' j) →
                                        autoParam
                                            (CategoryTheory.CategoryStruct.comp a (f' j) =
                                              CategoryTheory.CategoryStruct.comp q (f i))
                                            CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.mor._auto_1✝ →
                                          (F.presheafHom (D₁.obj i) (D₂.obj i)).obj
                                            (Opposite.op (CategoryTheory.Over.mk q))
-- Mathlib.Algebra.CharP.Algebra
charP_of_injective_algebraMap' : ∀ {A : Type u_2} (R : Type u_3) [inst : CommRing R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  (p : ℕ) [CharP R p], CharP A p
-- Init.Data.Array.MapIdx
Array.size_zipIdx : ∀ {α : Type u_1} {xs : Array α} {k : ℕ}, (xs.zipIdx k).size = xs.size
-- Lean.Elab.App
/-- Returns `true` if `fType` is a function type, possibly after applying `whnf` and updating `fType` if necessary.
It does not modify `fType` if it doesn't reduce to a function type, except to instantiate bvars.
Guarantees that the domain of the function type has no loose bvars.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.fTypeIsForall : Lean.Elab.Term.ElabAppArgs.M Bool
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.vcomp.inj : ∀ {B : Type u} {inst : Quiver B} {a b : CategoryTheory.FreeBicategory B} {f g h : a ⟶ b}
  {η : CategoryTheory.FreeBicategory.Hom₂ f g} {θ : CategoryTheory.FreeBicategory.Hom₂ g h} {g_1 : a ⟶ b}
  {η_1 : CategoryTheory.FreeBicategory.Hom₂ f g_1} {θ_1 : CategoryTheory.FreeBicategory.Hom₂ g_1 h},
  η.vcomp θ = η_1.vcomp θ_1 → g = g_1 ∧ η ≍ η_1 ∧ θ ≍ θ_1
-- Mathlib.Data.Finsupp.Interval
Finsupp.card_uIcc : ∀ {ι : Type u_1} {α : Type u_2} [inst : Lattice α] [inst_1 : Zero α] [inst_2 : LocallyFiniteOrder α] (f g : ι →₀ α),
  (Finset.uIcc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.uIcc (f i) (g i)).card
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for bitwise not of `BitVec`s.  -/
BitVec.reduceNot : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.left.eq_1 : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (X : CategoryTheory.Arrow T), X.left = X.left
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.isBigO_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f → ∀ (l : Filter E) (x : E), (fun x' => f (x' - x)) =O[l] fun x' => x' - x
-- Mathlib.Topology.Category.TopCat.OpenNhds
/-- The preimage functor from neighborhoods of `f x` to neighborhoods of `x`.  -/
TopologicalSpace.OpenNhds.map : {X Y : TopCat} →
  (f : X ⟶ Y) →
    (x : ↑X) →
      CategoryTheory.Functor (TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x))
        (TopologicalSpace.OpenNhds x)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.sigmaOpenCover_I₀ : ∀ {σ : Type v} (g : σ → AlgebraicGeometry.Scheme) [inst : Small.{u, v} σ], (AlgebraicGeometry.sigmaOpenCover g).I₀ = σ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : β k → β k} {fallback : α},
      (Std.DTreeMap.Internal.Impl.modify k f t).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.summable_nat_add_iff : ∀ {f : ℕ → NNReal} (k : ℕ), (Summable fun i => f (i + k)) ↔ Summable f
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.localInverse_apply_image : ∀ {𝕜 : 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] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  HasStrictFDerivAt.localInverse f f' a hf (f a) = a
-- Mathlib.GroupTheory.Congruence.Defs
/-- The subtraction induced on the quotient by an additive congruence relation on a
type with a subtraction.  -/
AddCon.hasSub : {M : Type u_1} → [inst : AddGroup M] → (c : AddCon M) → Sub c.Quotient
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_X_left_eq_map : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (p : Polynomial R),
  (Polynomial.aeval Polynomial.X) p = Polynomial.map (algebraMap R S) p
-- Init.Data.Bool
Bool.le_refl : ∀ (x : Bool), x ≤ x
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
MeasureTheory.Measure.iInf_rat_gt_prod_Iic : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} [MeasureTheory.IsFiniteMeasure ρ]
  {s : Set α}, MeasurableSet s → ∀ (t : ℚ), ⨅ r, ρ (s ×ˢ Set.Iic ↑↑r) = ρ (s ×ˢ Set.Iic ↑t)
-- Mathlib.Topology.Homotopy.HSpaces
/-- This is the function analogous to the one on p. 475 of [serre1951], defining a homotopy from
the product path `γ ∧ e` to `γ`.  -/
Path.delayReflRight : {X : Type u} → [inst : TopologicalSpace X] → {x y : X} → ↑unitInterval → Path x y → Path x y
-- Mathlib.Algebra.AddConstMap.Basic
/-- Change constants `a` and `b` in `(f : G →+c[a, b] H)` to improve definitional equalities.  -/
AddConstMap.replaceConsts : {G : Type u_1} →
  {H : Type u_2} →
    [inst : Add G] →
      [inst_1 : Add H] →
        {a : G} → {b : H} → AddConstMap G H a b → (a' : G) → (b' : H) → a = a' → b = b' → AddConstMap G H a' b'
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasFDerivAt.rpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {p : ℝ}, HasFDerivAt f f' x → f x ≠ 0 ∨ 1 ≤ p → HasFDerivAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • f') x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.finsetProd : ∀ {α : Type u_1} {l : Filter α} {ι : Type u_17} {R : Type u_18} {𝕜 : Type u_19} [inst : SeminormedCommRing R]
  [inst_1 : NormedField 𝕜] {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜},
  (∀ i ∈ s, f i =O[l] g i) → (fun x => ∏ i ∈ s, f i x) =O[l] fun x => ∏ i ∈ s, g i x
-- Mathlib.Topology.Irreducible
IsOpenMap.denseRange_of_isPreirreducibleSpace : ∀ {U : Type u_3} {X : Type u_4} [inst : TopologicalSpace U] [Nonempty U] [inst_2 : TopologicalSpace X] (f : U → X),
  IsOpenMap f → ∀ [PreirreducibleSpace X], DenseRange f
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.response : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Std.Channel (Except IO.Error (Std.Http.Response β))
-- Mathlib.RingTheory.Lasker
/-- The Lasker--Noether theorem: every submodule in a Noetherian module admits a decomposition into
primary submodules.  -/
Submodule.isLasker : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M],
  IsLasker R M
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (a : α),
  t.contains a = Std.DTreeMap.Internal.Impl.contains a t.inner
-- Mathlib.Algebra.Module.Injective
_private.Mathlib.Algebra.Module.Injective.0.Module.Baer.extensionOfMax_adjoin.aux1 : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) {f : M →ₗ[R] Q} [inst_7 : Fact (Function.Injective ⇑i)] {y : N}
  (x : ↥(Module.Baer.supExtensionOfMaxSingleton i f y)), ∃ a b, ↑x = ↑a + b • y
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- The norm of a function is controlled by the supremum of the pointwise norms.  -/
BoundedContinuousFunction.norm_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  {f : BoundedContinuousFunction α β} {C : ℝ}, 0 ≤ C → (‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C)
-- Lean.DocString.Extension
Lean.instReprElabBlock : Repr Lean.ElabBlock