mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Non-commutative version of `fderivWithin_inv`  -/
fderivWithin_inv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedDivisionRing R]
  [inst_2 : NormedAlgebra 𝕜 R] {s : Set R} {x : R},
  x ≠ 0 →
    UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (fun x => x⁻¹) s x = -((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.pi_lineMap_apply : ∀ {k : Type u_1} [inst : Ring k] {ι : Type u_10} {V : ι → Type u_11} {P : ι → Type u_12}
  [inst_1 : (i : ι) → AddCommGroup (V i)] [inst_2 : (i : ι) → Module k (V i)] [inst_3 : (i : ι) → AddTorsor (V i) (P i)]
  (f g : (i : ι) → P i) (c : k) (i : ι), (AffineMap.lineMap f g) c i = (AffineMap.lineMap (f i) (g i)) c
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- `liftToFinset`, when composed with the evaluation functor, results in the whiskering composed
with `colim`.  -/
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetEvaluationIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (α : Type w) →
      [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
        (I : Finset (CategoryTheory.Discrete α)) →
          (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α).comp
              ((CategoryTheory.evaluation (Finset (CategoryTheory.Discrete α))ᵒᵖ C).obj (Opposite.op I)) ≅
            ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Discrete ↥I) (CategoryTheory.Discrete α) C).obj
                  (CategoryTheory.Discrete.functor fun x => ↑x)).comp
              CategoryTheory.Limits.lim
-- Mathlib.Order.Nucleus
Nucleus.instSemilatticeInf : {X : Type u_1} → [inst : SemilatticeInf X] → SemilatticeInf (Nucleus X)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.splitAtPred.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α × Option α × List α → Sort u_2) (l₁ : List α) (o : Option α) (l₂ : List α)
  (h_1 : (l₁ : List α) → (o : Option α) → (l₂ : List α) → motive (l₁, o, l₂)),
  (match (l₁, o, l₂) with
    | (l₁, o, l₂) => h_1 l₁ o l₂) =
    h_1 l₁ o l₂
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- A `R`-bialgebra homomorphism from `A[M]` is uniquely defined by its
values on the functions `single m 1` and `single 1 a`.

See note [partially-applied ext lemmas]. Note that the first assumption isn't written as an
equality of `AddMonoidHom`s because `of` doesn't multiplicativise.  -/
AddMonoidAlgebra.bialgHom_ext : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] [inst_5 : AddMonoid M]
  ⦃φ₁ φ₂ : AddMonoidAlgebra A M →ₐc[R] B⦄,
  (∀ (m : M), φ₁ (AddMonoidAlgebra.single m 1) = φ₂ (AddMonoidAlgebra.single m 1)) →
    (↑φ₁).comp AddMonoidAlgebra.singleZeroAlgHom = (↑φ₂).comp AddMonoidAlgebra.singleZeroAlgHom → φ₁ = φ₂
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_injective : ∀ {R : Type u} [inst : Semiring R], Function.Injective Polynomial.coeff
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcKeepAliveParams.sessionId : Lean.Lsp.RpcKeepAliveParams → UInt64
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_rankPos : ∀ {α : Type u_1} {E : Set α}, E.Nonempty → (Matroid.freeOn E).RankPos
-- Mathlib.Order.Ideal
Order.Ideal.mem_toIdeal : ∀ {P : Type u_1} [inst : LE P] {I : Set P} (h : Order.IsIdeal I) {a : P}, a ∈ h.toIdeal ↔ a ∈ I
-- Mathlib.Topology.Separation.Basic
nhdsWithin_insert_of_ne : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X} {s : Set X},
  x ≠ y → nhdsWithin x (insert y s) = nhdsWithin x s
-- Mathlib.Analysis.Normed.Module.Bases
SchauderBasis.RankOneDecomposition.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] [inst_3 : SizeOf 𝕜] [inst_4 : SizeOf X] (P : ℕ → X →L[𝕜] X) (e : ℕ → X)
  (proj_zero : P 0 = 0) (finrank_range : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n)
  (proj_comp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x)
  (proj_tendsto : ∀ (x : X), Filter.Tendsto (fun n => (P n) x) Filter.atTop (nhds x))
  (e_mem_range : ∀ (n : ℕ), e n ∈ (↑(SchauderBasis.succSub P n)).range) (e_ne_zero : ∀ (n : ℕ), e n ≠ 0),
  sizeOf
      { P := P, e := e, proj_zero := proj_zero, finrank_range := finrank_range, proj_comp := proj_comp,
        proj_tendsto := proj_tendsto, e_mem_range := e_mem_range, e_ne_zero := e_ne_zero } =
    1 + sizeOf proj_zero
-- Init.Data.UInt.Lemmas
UInt64.toFin.eq_1 : ∀ (x : UInt64), x.toFin = x.toBitVec.toFin
-- Lean.Elab.Level
Lean.Elab.Level.State.mk : Lean.NameGenerator → Lean.MetavarContext → List Lean.Name → Lean.Elab.Level.State
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.toSubmodule : {R : Type u} →
  [inst : CommRing R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {k : ℕ} → Module.Grassmannian R M k → Submodule R M
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOpEquiv_inverse_obj : ∀ {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 : CategoryTheory.Limits.Cone F.op),
  CategoryTheory.Limits.coconeOpEquiv.inverse.obj c = Opposite.op c.unop
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- The pregroupoid property is stable under composition  -/
Pregroupoid.comp : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : Pregroupoid H) {f g : H → H} {u v : Set H},
  self.property f u →
    self.property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → self.property (g ∘ f) (u ∩ f ⁻¹' v)
-- Lean.Environment
/-- Like `findAsyncCore?`; allocating tasks is (currently?) too costly to do always.  -/
_private.Lean.Environment.0.Lean.Environment.findTaskCore : Lean.Environment → Lean.Name → optParam Bool false → Task (Option Lean.AsyncConstantInfo)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.dist_eq : ∀ (x y : ℝ), dist x y = |x - y|
-- Mathlib.Data.Num.Bitwise
Num.instHShiftLeftNat : HShiftLeft Num ℕ Num
-- Mathlib.MeasureTheory.Covering.LiminfLimsup
/-- This is really an auxiliary result en route to `blimsup_cthickening_ae_le_of_eventually_mul_le`
(which is itself an auxiliary result en route to `blimsup_cthickening_mul_ae_eq`).

NB: The `: Set α` type ascription is present because of
https://github.com/leanprover-community/mathlib/issues/16932.  -/
blimsup_cthickening_ae_le_of_eventually_mul_le_aux : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop)
  {s : ℕ → Set α},
  (∀ (i : ℕ), IsClosed (s i)) →
    ∀ {r₁ r₂ : ℕ → ℝ},
      Filter.Tendsto r₁ Filter.atTop (nhdsWithin 0 (Set.Ioi 0)) →
        0 ≤ r₁ →
          ∀ {M : ℝ},
            0 < M →
              M < 1 →
                (∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i) →
                  Filter.blimsup (fun i => Metric.cthickening (r₁ i) (s i)) Filter.atTop p ≤ᵐ[μ]
                    Filter.blimsup (fun i => Metric.cthickening (r₂ i) (s i)) Filter.atTop p
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_iff_enorm_inv_mul_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {f : α → E} {a : Filter α} {b : E},
  Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖(f e)⁻¹ * b‖ₑ) a (nhds 0)
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- **Alias** of the reverse direction of `isGroupLikeElem_unitsInv`. -/
IsGroupLikeElem.unitsInv : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] {u : Aˣ},
  IsGroupLikeElem R ↑u → IsGroupLikeElem R ↑u⁻¹
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The isomorphism between the global sections of `M^~` and `M`.  -/
AlgebraicGeometry.tilde.isoTop : {R : CommRingCat} →
  (M : ModuleCat ↑R) →
    M ≅ (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.obj (Opposite.op ⊤)
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- In a locally compact space, any integrable function can be approximated by compactly supported
continuous functions, version in terms of `∫⁻`.  -/
MeasureTheory.Integrable.exists_hasCompactSupport_lintegral_sub_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α]
  [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E},
  MeasureTheory.Integrable f μ →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ g, HasCompactSupport g ∧ ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
-- Aesop.Tree.Data
Aesop.NodeState.isProven : Aesop.NodeState → Bool
-- Lean.Elab.Command
Lean.Elab.Command.instNonemptyState : Nonempty Lean.Elab.Command.State
-- Init.Data.UInt.Lemmas
UInt8.add_right_inj : ∀ {a b : UInt8} (c : UInt8), c + a = c + b ↔ a = b
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coe_coeffsIn : ∀ {R : Type u_2} {S : Type u_3} (σ : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  (M : Submodule R S), ↑(MvPolynomial.coeffsIn σ M) = {p | ∀ (i : σ →₀ ℕ), MvPolynomial.coeff i p ∈ M}
-- Mathlib.RingTheory.Multiplicity
/-- **Alias** of `FiniteMultiplicity.not_isUnit`. -/
FiniteMultiplicity.not_unit : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b → ¬IsUnit a
-- Mathlib.RepresentationTheory.Induced
/-- Given a group homomorphism `φ : G →* H` and a `G`-representation `(A, ρ)`, this is the
`k`-module `(k[H] ⊗[k] A)_G` with the `G`-representation on `k[H]` defined by `φ`.
See `Representation.ind` for the induced `H`-representation on `IndV φ ρ`.  -/
Representation.IndV : {k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : Group H] →
            (G →* H) →
              {A : Type u_4} →
                [inst_3 : AddCommGroup A] → [inst_4 : Module k A] → Representation k G A → Type (max u_4 u_3 u_1)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {s₁ s₂ : Finset β} {f : β → α},
  s₁ ⊆ s₂ → s₁.sup f ≤ s₂.sup f
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.permutationsAux2.match_3.eq_2 : ∀ {α : Type u_1} {β : Type u_3} (motive : List α → (List α → β) → Sort u_2) (y : α) (ys : List α) (f : List α → β)
  (h_1 : (x : List α → β) → motive [] x) (h_2 : (y : α) → (ys : List α) → (f : List α → β) → motive (y :: ys) f),
  (match y :: ys, f with
    | [], x => h_1 x
    | y :: ys, f => h_2 y ys f) =
    h_2 y ys f
-- Std.Time.Time.Unit.Minute
/-- Creates an `Ordinal` from an integer, ensuring the value is within bounds.
 -/
Std.Time.Minute.Ordinal.ofInt : (data : ℤ) → 0 ≤ data ∧ data ≤ 59 → Std.Time.Minute.Ordinal
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonTypeDefinitionParams.fromJson : Lean.Json → Except String Lean.Lsp.TypeDefinitionParams
-- Mathlib.Algebra.GroupWithZero.Regular
/-- A right-regular element of a `Nontrivial` `MulZeroClass` is non-zero.  -/
IsRightRegular.ne_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] {a : R} [Nontrivial R], IsRightRegular a → a ≠ 0
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- In an `S` algebra `R`, the order of vanishing of `x : R` is less than or equal
to the order of vanishing of `a • x` for any `a : S`. One should note that the order here
is the order on `ℕ∞` where `∞` is a top element.
 -/
Ring.ord_le_smul : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_3} [inst_1 : CommRing S] [inst_2 : Algebra S R] (a : S) (x : R),
  Ring.ord R x ≤ Ring.ord R (a • x)
-- Batteries.Recycling.RBTree.WF
/-- The `reverse` function reverses the ordering invariants.  -/
RBTree.RBNode.Ordered.reverse : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t → RBTree.RBNode.Ordered (flip cmp) t.reverse
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.mem_sup : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L} {x : X}, x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
Lean.Meta.Grind.isMarkedSubsingletonApp : Lean.Expr → Bool
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.e.eq_1 : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ), A.e = ↑A.snd
-- Mathlib.SetTheory.Cardinal.Finite
ENat.one_lt_card_iff_nontrivial : ∀ (α : Type u_3), 1 < ENat.card α ↔ Nontrivial α
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_id : ∀ {α : Type u_1} {l : Filter α}, Filter.EventuallyConst id l ↔ l.Subsingleton
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.le_rpow_inv_iff_of_pos : ∀ {z : ℝ} {y : NNReal}, 0 ≤ y → 0 < z → ∀ (x : NNReal), x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableAtom_eq_of_mem : ∀ {β : Type u_2} [inst : MeasurableSpace β] {x y : β}, x ∈ measurableAtom y → measurableAtom x = measurableAtom y
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.ShouldCanonResult.canonType : Lean.Meta.Sym.Canon.ShouldCanonResult✝
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_last : ∀ {n : ℕ} {α : Fin (n + 2) → Sort u_1} (x : α 0) (p : (i : Fin n.succ) → α i.succ),
  Fin.cons x p (Fin.last (n + 1)) = p (Fin.last n)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
ContinuousLinearMap.IsIdempotentElem.isClosed_range : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [IsTopologicalAddGroup M] [T1Space M] {p : M →L[R] M}, IsIdempotentElem p → IsClosed ↑(↑p).range
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.finset_logSizeBallSeq_add_one_ssubset : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ),
  (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty →
    (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset ⊂ (PairReduction.logSizeBallSeq J hJ a c i).finset
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.EStateM.instWP.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → motive (EStateM.Result.ok a s')) →
        ((e : ε) → (s' : σ) → motive (EStateM.Result.error e s')) → motive x
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux1.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option (Computation α))) → Sort u_2)
  (x : Option (Stream'.Seq1 (Option (Computation α)))) (h_1 : Unit → motive none)
  (h_2 : (S' : Stream'.Seq (Option (Computation α))) → motive (some (none, S')))
  (h_3 : (c : Computation α) → (S' : Stream'.Seq (Option (Computation α))) → motive (some (some c, S'))),
  x = none →
    (match x with
      | none => h_1 ()
      | some (none, S') => h_2 S'
      | some (some c, S') => h_3 c S') ≍
      h_1 ()
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerLeft_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] (F : CategoryTheory.Functor C D)
  {G H : CategoryTheory.Functor D E} (α : G ⟶ H) (X : C), (F.whiskerLeft α).app X = α.app (F.obj X)
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_three_eval_one_quarter : Polynomial.eval (1 / 4) (Polynomial.bernoulli 3) = 3 / 64
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
ContinuousAt.log : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {a : α},
  ContinuousAt f a → f a ≠ 0 → ContinuousAt (fun x => Real.log (f x)) a
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_assoc_flip_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.MonObj.mul)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul M)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h))
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
/-- The underlying map of an affine map between convex spaces.  -/
Convexity.ConvexSpace.AffineMap.toFun : {R : Type u_1} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        {X : Type u_2} →
          {Y : Type u_3} →
            [inst_3 : Convexity.ConvexSpace R X] →
              [inst_4 : Convexity.ConvexSpace R Y] → Convexity.ConvexSpace.AffineMap R X Y → X → Y
-- Std.Data.TreeMap.Basic
/-- Erases multiple mappings from the tree map by iterating over the given collection and calling
`erase`.
 -/
Std.TreeMap.eraseMany : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.TreeMap α β cmp → ρ → Std.TreeMap α β cmp
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (hom hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i) (e_hom : hom = hom_1)
  (comm :
    ∀ (i₁ i₂ : ι),
      CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom i₁)) (D₂.hom i₁ i₂) =
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom i₂))),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Std.Http.Data.Body.Stream
/-- Context-aware iteration over chunks until the channel closes.
 -/
Std.Http.Body.Stream.forIn' : {β : Type} →
  Std.Http.Body.Stream → β → (Std.Http.Chunk → β → Std.Async.ContextAsync (ForInStep β)) → Std.Async.ContextAsync β
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.Respects.toRespectsLeft : ∀ {C : Type u} {inst : CategoryTheory.CategoryStruct.{v, u} C} {P Q : CategoryTheory.MorphismProperty C}
  [self : P.Respects Q], P.RespectsLeft Q
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.liftR_iff : ∀ {n : ℕ} {F : TypeVec.{u} n → Type u_1} [q : MvQPF F] {α : TypeVec.{u} n} (r : ⦃i : Fin2 n⦄ → α i → α i → Prop)
  (x y : F α),
  MvFunctor.LiftR r x y ↔
    ∃ a f₀ f₁,
      x = MvQPF.abs ⟨a, f₀⟩ ∧ y = MvQPF.abs ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : (MvQPF.P F).B a i), r (f₀ i j) (f₁ i j)
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Simplified to `e'`. If `done = true`, skip recursive simplification of `e'`.  -/
Lean.Meta.Sym.DSimp.Result.step : Lean.Expr → optParam Bool false → Lean.Meta.Sym.DSimp.Result
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalk_mono_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type v} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  [instCC : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] [CategoryTheory.Limits.HasLimits C]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  {F G : TopCat.Sheaf C X} (f : F ⟶ G) [CategoryTheory.Mono f] (x : ↑X),
  CategoryTheory.Mono ((TopCat.Presheaf.stalkFunctor C x).map f.hom)
-- Init.Core
/-- The inverse image of `r : β → β → Prop` by a function `α → β` is the relation
`s : α → α → Prop` defined by `s a b = r (f a) (f b)`.
 -/
InvImage : {α : Sort u} → {β : Sort v} → (β → β → Prop) → (α → β) → α → α → Prop
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.singleOneAlgHom.eq_1 : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M], MonoidAlgebra.singleOneAlgHom = { toRingHom := MonoidAlgebra.singleOneRingHom, commutes' := ⋯ }
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.ker_eval₂Hom_universalFactorizationMap : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  RingHom.ker
      (MvPolynomial.eval₂Hom (↑(MvPolynomial.universalFactorizationMap R n m k hn))
        (Sum.elim (fun x => MvPolynomial.X x ⊗ₜ[R] 1) fun x => 1 ⊗ₜ[R] MvPolynomial.X x)) =
    Ideal.span
      (Set.range fun i =>
        MvPolynomial.C (MvPolynomial.X i) -
          (MvPolynomial.map MvPolynomial.C)
            ((MvPolynomial.tensorEquivSum R (Fin m) (Fin k) R)
              ((MvPolynomial.universalFactorizationMap R n m k hn) (MvPolynomial.X i))))
-- Mathlib.Topology.Algebra.Group.Matrix
Topology.IsClosedEmbedding.specialLinearGroup_map : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] {f : R →+* S} [IsTopologicalRing R]
  [T1Space R], Topology.IsClosedEmbedding ⇑f → Topology.IsClosedEmbedding ⇑(Matrix.SpecialLinearGroup.map f)
-- Mathlib.Data.TypeVec
/-- arrow that rearranges the type of `Subtype_` to turn a subtype of vector into
a vector of subtypes  -/
TypeVec.toSubtype : {n : ℕ} →
  {α : TypeVec.{u} n} →
    (p : α.Arrow (TypeVec.repeat n Prop)) →
      TypeVec.Arrow (fun i => { x // TypeVec.ofRepeat (p i x) }) (TypeVec.Subtype_ p)
-- Init.Data.Rat.Lemmas
Rat.neg_mkRat : ∀ (n : ℤ) (d : ℕ), -mkRat n d = mkRat (-n) d
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.colorable_iff_exists_bdd_nat_coloring : ∀ {V : Type u} {G : SimpleGraph V} (n : ℕ), G.Colorable n ↔ ∃ C, ∀ (v : V), C v < n
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.omega_re : ∀ {R : Type u_2} {a b : R} [inst : Zero R] [inst_1 : One R], QuadraticAlgebra.omega.re = 0
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.Const.insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ α]
  {m : Std.DHashMap.Raw α fun x => Unit} {l : ρ}, m.WF → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).WF
-- Mathlib.Topology.MetricSpace.Bounded
/-- A compact set is bounded  -/
IsCompact.isBounded : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsCompact s → Bornology.IsBounded s
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary
definition for the main definition `adjoint`, where this is bundled as a conjugate-linear isometric
equivalence.  -/
_private.Mathlib.Analysis.InnerProductSpace.Adjoint.0.ContinuousLinearMap.adjointAux : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : InnerProductSpace 𝕜 E] →
              [inst_4 : InnerProductSpace 𝕜 F] → [CompleteSpace E] → (E →L[𝕜] F) →L⋆[𝕜] F →L[𝕜] E
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The factorization axiom for two classes of morphisms `W₁` and `W₂` in a category `C`. It
asserts that any morphism can be factored as a morphism in `W₁` followed by a morphism
in `W₂`.  -/
CategoryTheory.MorphismProperty.HasFactorization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Analysis.Normed.Group.Continuity
SeminormedAddCommGroup.mem_closure_iff : ∀ {E : Type u_4} [inst : SeminormedAddCommGroup E] {a : E} {s : Set E},
  a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a - b‖ < ε