mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Environment
/-- Like `evalConst`, but first check that `constName` indeed is a declaration of type `typeName`.
Note that this function cannot guarantee that `typeName` is in fact the name of the type `α`.  -/
Lean.Environment.evalConstCheck : (α : Type) → Lean.Environment → Lean.Options → Lean.Name → Lean.Name → ExceptT String Id α
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.ext_of_fromSpecResidueField_eq : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) (i : Y ⟶ Z) [AlgebraicGeometry.IsSeparated i]
  [AlgebraicGeometry.IsReduced X] (S : Set ↥X),
  Dense S →
    (∀ x ∈ S,
        CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f =
          CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) g) →
      CategoryTheory.CategoryStruct.comp f i = CategoryTheory.CategoryStruct.comp g i → f = g
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (f : S ⟶ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T),
  ((CategoryTheory.StructuredArrow.map f).obj X).right = X.right
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.smul_univ₀' : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : GroupWithZero α] [inst_2 : MulAction α β]
  [inst_3 : Fintype β] {s : Finset α}, s.Nontrivial → s • Finset.univ = Finset.univ
-- Lean.Log
/-- Log a new error message using the given message data. The position is provided by `ref`.  -/
Lean.logErrorAt : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Syntax → Lean.MessageData → m Unit
-- Lean.MetavarContext
Lean.MetavarContext.getExprAssignmentExp : Lean.MetavarContext → Lean.MVarId → Option Lean.Expr
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instSup : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace β] → [inst_2 : SemilatticeSup β] → [ContinuousSup β] → Max (α →ₘ[μ] β)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.model_nonempty : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] [h : Nonempty M], M ⊨ L.nonemptyTheory
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.coe_id : ∀ (V : SemiNormedGrp₁), ⇑↑(SemiNormedGrp₁.Hom.hom (CategoryTheory.CategoryStruct.id V)) = id
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.congr_fun : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  {f g : A →ₑ*[φ] B}, f = g → ∀ (x : A), f x = g x
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.adjoin.congr_simp : ∀ (k : Type u_1) {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (s s_1 : Set K) (e_s : s = s_1) [inst_4 : Finite ↑s],
  FiniteGaloisIntermediateField.adjoin k s = FiniteGaloisIntermediateField.adjoin k s_1
-- Aesop.Index.Forward
Aesop.instInhabitedForwardIndex : Inhabited Aesop.ForwardIndex
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.wellFoundedOn_devosAddRel : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α],
  {x | x.1.Nonempty ∧ x.2.Nonempty}.WellFoundedOn DevosAddRel✝
-- Mathlib.Algebra.Group.Defs
/-- An alternative to `mul_comm` which uses the mixin `IsMulCommutative` instead of bundled
commutative algebraic structures. In general, you should prefer `mul_comm` unless you are working
with commutative subobjects in a noncommutative algebraic structure.  -/
mul_comm' : ∀ {M : Type u_2} [inst : Mul M] [IsMulCommutative M] (a b : M), a * b = b * a
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.linearEquivMap_symm_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) [inst_5 : Module.FinitePresentation R M]
  (f : M →ₗ[R] N),
  (Module.FinitePresentation.linearEquivMap S).symm
      ((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)) f) =
    (LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f
-- Mathlib.CategoryTheory.Sites.SheafHom
/-- The sections of the presheaf `presheafHom F G` identify to morphisms `F ⟶ G`.  -/
CategoryTheory.presheafHomSectionsEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        (F G : CategoryTheory.Functor Cᵒᵖ A) → ↑(CategoryTheory.presheafHom F G).sections ≃ (F ⟶ G)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_subset_Iio_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio b ⊆ Set.Iio a ↔ b ≤ a
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.eq_1 : ∀ {α : Type u_1} (f g : Equiv.Perm α), f.Disjoint g = ∀ (x : α), f x = x ∨ g x = x
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- **Alias** of `AddSubgroup.range_subtype`. -/
AddSubgroup.subtype_range : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.subtype.range = H
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (k : α) [inst_1 : Inhabited α],
  t.getKey! k =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.getKey!" 186 13
        "Key is not present in map"
    | Std.DTreeMap.Internal.Impl.inner size k' v l r =>
      match compare k k' with
      | Ordering.lt => l.getKey! k
      | Ordering.gt => r.getKey! k
      | Ordering.eq => k'
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid.dual_iff : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α}, t.Valid ↔ t.dual.Valid
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- We say `C` has strict terminal objects if every terminal object is strict, i.e. given any
morphism `f : I ⟶ A` where `I` is terminal, then `f` is an isomorphism.

Strictly speaking, this says that *any* terminal object must be strict, rather than that strict
terminal objects exist.
 -/
CategoryTheory.Limits.HasStrictTerminalObjects : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonSlice : Lean.FromJson String.Slice
-- Mathlib.Order.Filter.Basic
Filter.NeBot.nonempty : ∀ {α : Type u} (f : Filter α) [hf : f.NeBot], Nonempty α
-- Mathlib.CategoryTheory.Monoidal.Closed.Types
/-- The adjunction `tensorLeft.obj X ⊣ coyoneda.obj (Opposite.op X)`
for any `X : Type v₁`.  -/
CategoryTheory.Types.tensorProductAdjunction : (X : Type v₁) → CategoryTheory.MonoidalCategory.tensorLeft X ⊣ CategoryTheory.coyoneda.obj (Opposite.op X)
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken : Type
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} {ι : Type u_1} {Y : ι → C} (f : (i : ι) → Y i ⟶ X),
  CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.ofArrows Y f) =
    CategoryTheory.Sieve.ofArrows (fun i => F.obj (Y i)) fun i => F.map (f i)
-- Std.Http.Protocol.H1.Parser
Std.Http.Protocol.H1.TakeResult.complete.sizeOf_spec : ∀ (data : ByteSlice), sizeOf (Std.Http.Protocol.H1.TakeResult.complete data) = 1 + sizeOf data
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The iterated derivative within a set of the composition with a linear map on the left is
obtained by applying the linear map to the iterated derivative.  -/
ContinuousLinearMap.iteratedFDerivWithin_comp_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x : E} {n : WithTop ℕ∞} {f : E → F}
  (g : F →L[𝕜] G),
  ContDiffWithinAt 𝕜 n f s x →
    UniqueDiffOn 𝕜 s →
      x ∈ s →
        ∀ {i : ℕ},
          ↑i ≤ n →
            iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
-- Mathlib.Topology.Order.LeftRightNhds
nhds_eq_iInf_mabs_div : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α]
  [OrderTopology α] (a : α), nhds a = ⨅ r, ⨅ (_ : r > 1), Filter.principal {b | |a / b|ₘ < r}
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- Close the goal of the form `η = θ`, where `η` and `θ` are 2-isomorphisms made up only of
associators, unitors, and identities.  -/
Mathlib.Tactic.BicategoryLike.pureCoherence : (ρ : Type) →
  [Mathlib.Tactic.BicategoryLike.Context ρ] →
    [Mathlib.Tactic.BicategoryLike.MkMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
      [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
        [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
          [Mathlib.Tactic.BicategoryLike.MonadCoherehnceHom (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
            [Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
              [Mathlib.Tactic.BicategoryLike.MkEqOfNaturality (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
                Lean.Name → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.RestrictionCoextensionAdj.counit'.eq_1 : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  ModuleCat.RestrictionCoextensionAdj.counit' f =
    {
      app := fun X =>
        ModuleCat.ofHom
          { toFun := fun g => ((ModuleCat.CoextendScalars.equiv f X) g) 1, map_add' := ⋯, map_smul' := ⋯ },
      naturality := ⋯ }
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [IsDomain R] [IsDomain T] [inst_5 : Algebra R S] {P : Ideal R} [inst_6 : P.IsPrime] [inst_7 : Algebra S T]
  [inst_8 : Algebra R T] [inst_9 : IsScalarTower R S T] [Module.IsTorsionFree R T],
  IsScalarTower (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
    (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.get : {α : Type} → Lean.VisibilityMap✝ α → Lean.Environment → α
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_slice : ∀ {m : Type w → Type x} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {γ : Type u}
  {α β : Type w} [LawfulMonad m] {δ : Type w} [inst_3 : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_4 : Std.Iterator α Id β] [inst_5 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  [Std.Iterators.Finite α Id] {init : δ} {f : β → δ → m (ForInStep δ)} {xs : Std.Slice γ}
  (inv : Std.Do.Invariant xs.toList δ ps),
  (∀ (pref : List β) (cur : β) (suff : List β) (h : xs.toList = pref ++ cur :: suff) (b : δ),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAtFilter.isBigOTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {L : Filter (E × E)} [ContinuousAdd F]
  [ContinuousSMul 𝕜 F], HasFDerivAtFilter f f' L → (fun p => f p.1 - f p.2) =O[𝕜; L] fun p => p.1 - p.2
-- Mathlib.RingTheory.Polynomial.HilbertPoly
/-- The function that sends any `p : F[X]` to `Polynomial.hilbertPoly p d` is an `F`-linear map from
`F[X]` to `F[X]`.
 -/
Polynomial.hilbertPoly_linearMap : (F : Type u_1) → [inst : Field F] → ℕ → Polynomial F →ₗ[F] Polynomial F
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coordChangeL_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e]
  [inst_9 : Bundle.Trivialization.IsLinear R e'] {b : B},
  b ∈ e.baseSet ∩ e'.baseSet → ∀ (y : F), (Bundle.Trivialization.coordChangeL R e e' b) y = (↑e' ⟨b, e.symm b y⟩).2
-- Init.Data.BitVec.Lemmas
BitVec.getElem_sshiftRight : ∀ {w : ℕ} {x : BitVec w} {s i : ℕ} (h : i < w), (x.sshiftRight s)[i] = if h : s + i < w then x[s + i] else x.msb
-- Mathlib.Topology.Algebra.Star.Unitary
instIsTopologicalGroupSubtypeMemSubmonoidUnitaryOfContinuousMulOfContinuousStar : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : TopologicalSpace R] [ContinuousMul R]
  [ContinuousStar R], IsTopologicalGroup ↥(unitary R)
-- Mathlib.Algebra.Jordan.Basic
/-- A (non-commutative) Jordan multiplication.  -/
IsJordan : (A : Type u_1) → [Mul A] → Prop
-- Mathlib.Data.Real.Basic
Real.instNatCast : NatCast ℝ
-- Mathlib.Data.Sigma.Basic
/-- Map the left and right components of a sigma  -/
PSigma.map : {α₁ : Sort u_3} →
  {α₂ : Sort u_4} →
    {β₁ : α₁ → Sort u_5} → {β₂ : α₂ → Sort u_6} → (f₁ : α₁ → α₂) → ((a : α₁) → β₁ a → β₂ (f₁ a)) → PSigma β₁ → PSigma β₂
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableAt.cle_arrowCongr : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_17}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {f : M → F₁ ≃L[𝕜] F₂} {g : M → F₃ ≃L[𝕜] F₄} {x : M},
  (MDiffAt fun x => ↑(f x).symm) x → (MDiffAt fun x => ↑(g x)) x → (MDiffAt fun y => ↑((f y).arrowCongr (g y))) x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β}, m.contains a = false → m.getD a fallback = fallback
-- Mathlib.Data.Int.Cast.Basic
zsmul_one : ∀ {R : Type u_1} [inst : AddGroupWithOne R] (n : ℤ), n • 1 = ↑n
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.aeval_one_tmul : ∀ (R : Type u) {N : Type v} [inst : CommSemiring R] {σ : Type u_1} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : CommSemiring N] [inst_4 : Algebra R N] (f : σ → S) (p : MvPolynomial σ R),
  (MvPolynomial.aeval fun x => 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (MvPolynomial.aeval f) p
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then
`f` is an antitone function.  -/
antitone_of_deriv_nonpos : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → (∀ (x : ℝ), deriv f x ≤ 0) → Antitone f
-- Mathlib.Topology.MetricSpace.Defs
/-- Deduce the equality of points from the vanishing of the nonnegative distance  -/
eq_of_nndist_eq_zero : ∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, nndist x y = 0 → x = y
-- Lean.Expr
Lean.Nat.mkInstLT : Lean.Expr
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap.eq_1 : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : Field β]
  [inst_3 : ConditionallyCompleteLinearOrder β] (x : α),
  ConditionallyCompleteLinearOrderedField.inducedMap α β x = sSup (LinearOrderedField.cutMap β x)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : OmegaCompletePartialOrder α]
  [inst_1 : OmegaCompletePartialOrder β] [inst_2 : OmegaCompletePartialOrder γ] {f : α → β} {g : β → γ},
  OmegaCompletePartialOrder.ωScottContinuous g →
    OmegaCompletePartialOrder.ωScottContinuous f → OmegaCompletePartialOrder.ωScottContinuous (g ∘ f)
-- Std.Http.Data.Body.Basic
/-- Receives the next body chunk. Returns `none` at end-of-stream.
 -/
Std.Http.Body.recv : {α : Type} → [self : Std.Http.Body α] → α → Std.Async.Async (Option Std.Http.Chunk)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_eq_getLast!_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.maxKey! = t.keys.getLast!
-- Mathlib.Data.ZMod.Basic
ZMod.cast_zmod_eq_zero_iff_of_le : ∀ {m n : ℕ} [NeZero m], m ≤ n → ∀ (a : ZMod m), a.cast = 0 ↔ a = 0
-- Mathlib.Computability.Primrec.List
Primrec.list_headI : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : Inhabited α], Primrec List.headI
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k},
  t.isEmpty = true → ∀ {fallback : α}, (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKeyD fallback = k
-- Mathlib.Algebra.Lie.Prod
LieEquiv.prodComm_invFun : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (a : L₂ × L₁), (LieEquiv.prodComm R L₁ L₂).invFun a = a.swap
-- Mathlib.NumberTheory.Divisors
Nat.Prime.prod_properDivisors : ∀ {α : Type u_1} [inst : CommMonoid α] {p : ℕ} {f : ℕ → α}, Nat.Prime p → ∏ x ∈ p.properDivisors, f x = f 1
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.IsEquivalenceRelation.nonempty_equivalenceRelation : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {R X : C} {p₁ p₂ : R ⟶ X}
  [self : CategoryTheory.IsEquivalenceRelation p₁ p₂], Nonempty (CategoryTheory.EquivalenceRelation p₁ p₂)
-- Mathlib.Data.Fintype.Quotient
Quotient.finRecOn_mk : ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  {C : ((i : ι) → Quotient (S i)) → Sort u_4} (a : (i : ι) → α i), (Quotient.finRecOn fun x => ⟦a x⟧) = fun f x => f a
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- If the set where you want `f` to be `C^n` lies entirely in a single chart, and `f` maps it
into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in
these charts.
Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
that this set lies in `(extChartAt I x).target`.  -/
contMDiffOn_iff_of_subset_source' : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {y : M'} {n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  s ⊆ (extChartAt I x).source →
    Set.MapsTo f s (extChartAt I' y).source →
      (ContMDiffOn I I' n f s ↔
        ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) '' s))
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.isIso_iff : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : DerivedCategory C} (f : K ⟶ L),
  CategoryTheory.IsIso f ↔ ∀ (n : ℤ), CategoryTheory.IsIso ((DerivedCategory.homologyFunctor C n).map f)
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonUnitalNonAssocCommRingWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} → {α : Type u_3} → [NonUnitalNonAssocCommRing α] → NonUnitalNonAssocCommRing (WithConv (Matrix m n α))
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_neg_right`. -/
Asymptotics.IsBigOWith.of_neg_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E}
  {g' : α → F'} {l : Filter α}, (Asymptotics.IsBigOWith c l f fun x => -g' x) → Asymptotics.IsBigOWith c l f g'
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- `exp ∘ f` is analytic  -/
AnalyticOnNhd.cexp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E},
  AnalyticOnNhd ℂ f s → AnalyticOnNhd ℂ (fun z => Complex.exp (f z)) s
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
/-- The variation of a vecture measure with density `f` with respect to a positive measure `μ`
is the measure with density `‖f‖ₑ` with respect to `μ`.  -/
MeasureTheory.Measure.variation_withDensityᵥ : ∀ {X : Type u_1} {E : Type u_2} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure X} {f : X → E},
  MeasureTheory.Integrable f μ → (μ.withDensityᵥ f).variation = μ.withDensity fun x => ‖f x‖ₑ
-- Mathlib.MeasureTheory.Group.Arithmetic
Finset.aemeasurable_prod : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, AEMeasurable (f i) μ) → AEMeasurable (∏ i ∈ s, f i) μ
-- Mathlib.RingTheory.WittVector.Teichmuller
WittVector.teichmuller_coeff_pos : ∀ (p : ℕ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (r : R) (n : ℕ),
  0 < n → ((WittVector.teichmuller p) r).coeff n = 0
-- Lean.Elab.InfoTree.Main
Lean.Elab.UserWidgetInfo.format : Lean.Elab.UserWidgetInfo → Std.Format
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Given a continuous function `g : β → γ → δ`, and almost everywhere equal functions
`[f₁] : α →ₘ β` and `[f₂] : α →ₘ γ`, return the equivalence class of the function
`fun a => g (f₁ a) (f₂ a)`, i.e., the almost everywhere equal function
`[fun a => g (f₁ a) (f₂ a)] : α →ₘ γ`  -/
MeasureTheory.AEEqFun.comp₂ : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        [inst : MeasurableSpace α] →
          {μ : MeasureTheory.Measure α} →
            [inst_1 : TopologicalSpace δ] →
              [inst_2 : TopologicalSpace β] →
                [inst_3 : TopologicalSpace γ] →
                  (g : β → γ → δ) → Continuous (Function.uncurry g) → (α →ₘ[μ] β) → (α →ₘ[μ] γ) → α →ₘ[μ] δ