mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Immersion
/-- Every `ModelWithCorners 𝕜 E H` is an immersion when viewed as a map `H → E`.  -/
ModelWithCorners.isImmersionAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : ℕ} {x : H},
  Manifold.IsImmersionAt I (modelWithCornersSelf 𝕜 E) (↑n) (↑I) x
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.mapM_eq_toIter_mapM_toIterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  [inst_2 : MonadAttach m] {f : β → m γ}, Std.Iter.mapM f it = Std.IterM.mapM f it.toIterM
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
/-- If `M : Cᴹᵒᵖ` is a monoid object, then `unmop M : C` too.  -/
MonObj.unmopMonObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (M : Cᴹᵒᵖ) → [CategoryTheory.MonObj M] → CategoryTheory.MonObj M.unmop
-- Aesop.Check
Aesop.Check.tree : Aesop.Check
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.linearEquiv.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1) {M : Type u_2} {M' : Type u_3}
  {M'' : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M'']
  [inst_4 : Module R M] [inst_5 : Module R M'] [inst_6 : Module R M''] (f f_1 : M →ₗ[R] M') (e_f : f = f_1)
  (g g_1 : M →ₗ[R] M'') (e_g : g = g_1) [inst_7 : IsLocalizedModule S f] [inst_8 : IsLocalizedModule S g],
  IsLocalizedModule.linearEquiv S f g = IsLocalizedModule.linearEquiv S_1 f_1 g_1
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instVAdd : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : (i : ι) → VAdd R (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] → VAdd R (DirectLimit G f)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_29 : HSub Std.Time.Hour.Offset Std.Time.Week.Offset Std.Time.Hour.Offset
-- Mathlib.Algebra.Ring.Ext
AddCommGroupWithOne.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : AddCommGroupWithOne R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ One.one = One.one
-- Aesop.Tracing
Aesop.TraceOption.rpinf : Aesop.TraceOption
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curry_uncurryRight : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
  (f : MultilinearMap R (fun i => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)), f.uncurryRight.curryRight = f
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.irrational_rpow_rat_rat_of_den : ∀ {x y : ℝ} {x_num x_den y_num y_den k_den : ℕ},
  Mathlib.Meta.NormNum.IsNNRat x x_num x_den →
    Mathlib.Meta.NormNum.IsNNRat y y_num y_den →
      x_num.Coprime x_den →
        y_num.Coprime y_den → k_den ^ y_den < x_den → x_den < (k_den + 1) ^ y_den → Irrational (x ^ y)
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_transpose : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A.transpose‖₊ = ‖A‖₊
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.order.eq_1 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F), p.order = sInf {n | p n ≠ 0}
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore_idempotent : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.normalCore.normalCore = H.normalCore
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- The functions in the partition of unity add up to `1` at any point of `s`.  -/
SmoothPartitionOfUnity.sum_eq_one' : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : optParam (Set M) Set.univ} (self : SmoothPartitionOfUnity ι I M s),
  ∀ x ∈ s, ∑ᶠ (i : ι), (self.toFun i) x = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le : ∀ {n d : ℕ} (S : ↑{S | S.card = d + 1}) (A : (SSet.stdSimplex.obj { len := n }).Subcomplex),
  ↑(SSet.stdSimplex.nonDegenerateEquiv'.symm S) ∈ A.obj (Opposite.op { len := d }) ↔ SSet.stdSimplex.face ↑S ≤ A
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.Bicone.left.sizeOf_spec : ∀ {J : Type u₁} [inst : SizeOf J], sizeOf CategoryTheory.Bicone.left = 1
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectR_prodMkLeft : ∀ {β : Type u_2} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (α : Type u_6)
  [inst : MeasurableSpace α] (κ : ProbabilityTheory.Kernel β γ) (a : α),
  (ProbabilityTheory.Kernel.prodMkLeft α κ).sectR a = κ
-- Init.Data.Random
/-- `range` returns the range of values returned by
the generator.  -/
RandomGen.range : {g : Type u} → [self : RandomGen g] → g → ℕ × ℕ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Unitization.inr_nonneg_iff : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : A}, 0 ≤ ↑a ↔ 0 ≤ a
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulLeftMap.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_5}
  (m : ι → ↥M), Submodule.mulLeftMap N m = (Finsupp.lsum R) fun i => ↑(m i) • N.subtype
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_zero_mul_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R) (s : σ),
  (MvPowerSeries.coeff 0) (φ * MvPowerSeries.X s) = 0
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- We say that a collection of `SmoothBumpFunction`s is a `SmoothBumpCovering` of a set `s` if

* `(f i).c ∈ s` for all `i`;
* the family `fun i ↦ support (f i)` is locally finite;
* for each point `x ∈ s` there exists `i` such that `f i =ᶠ[𝓝 x] 1`;
  in other words, `x` belongs to the interior of `{y | f i y = 1}`;

If `M` is a finite-dimensional real manifold which is a `σ`-compact Hausdorff topological space,
then for every covering `U : M → Set M`, `∀ x, U x ∈ 𝓝 x`, there exists a `SmoothBumpCovering`
subordinate to `U`, see `SmoothBumpCovering.exists_isSubordinate`.

This covering can be used, e.g., to construct a partition of unity and to prove the weak
Whitney embedding theorem.  -/
SmoothBumpCovering : Type uι →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            ModelWithCorners ℝ E H →
              (M : Type uM) →
                [inst_3 : TopologicalSpace M] →
                  [ChartedSpace H M] → [FiniteDimensional ℝ E] → optParam (Set M) Set.univ → Type (max uM uι)
-- Mathlib.Topology.Algebra.Monoid
SeparatelyContinuousMul.to_continuousSMul : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M], ContinuousConstSMul M M
-- Mathlib.Algebra.Opposites
MulOpposite.unop_op : ∀ {α : Type u_1} (x : α), MulOpposite.unop (MulOpposite.op x) = x
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.isRegularEpi_op_iff_isRegularMono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsRegularEpi f.op ↔ CategoryTheory.IsRegularMono f
-- Mathlib.Computability.EpsilonNFA
/-- `M.evalFrom S x` computes all possible paths through `M` with input `x` starting at an element
of `S`.  -/
εNFA.evalFrom : {α : Type u} → {σ : Type v} → εNFA α σ → Set σ → List α → Set σ
-- Mathlib.Geometry.Euclidean.SignedDist
/-- The signed distance between the face of `s` excluding point `i` of that simplex and a point,
in the direction of the reference point `i`. This is expected to be used when the point at which
the distance is evaluated lies in the affine span of the simplex (any component of the distance
orthogonal to that span is disregarded). In the case of a triangle, these distances are
trilinear coordinates; in a tetrahedron, they are quadriplanar coordinates.  -/
Affine.Simplex.signedInfDist : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → {n : ℕ} → [NeZero n] → Affine.Simplex ℝ P n → Fin (n + 1) → P →ᴬ[ℝ] ℝ
-- Mathlib.Topology.Coherent
Topology.IsCoherentWith.of_continuous_prop : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)},
  (∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous f) → Topology.IsCoherentWith S
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.compileDecls.doCompile : Array Lean.Name → Bool → Lean.CoreM Unit
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.monomial_mem_nonzeroDivisors : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {n : σ →₀ ℕ} {r : R},
  (MvPowerSeries.monomial n) r ∈ nonZeroDivisors (MvPowerSeries σ R) ↔ r ∈ nonZeroDivisors R
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.dense_source : ∀ {X Y : AlgebraicGeometry.Scheme} (self : X.PartialIso Y), Dense ↑self.source
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).getKey! k = if t₂.contains k = true then t₁.getKey! k else default
-- Init.Data.Vector.Basic
/-- Returns a vector of size `1` with element `v`.  -/
Vector.singleton : {α : Type u_1} → α → Vector α 1
-- Mathlib.Analysis.Convex.Combination
/-- A version of `Finset.centerMass_mem_convexHull` for when the weights are nonpositive.  -/
Finset.centerMass_mem_convexHull_of_nonpos : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {s : Set E} {w : ι → R} {z : ι → E} [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (t : Finset ι),
  (∀ i ∈ t, w i ≤ 0) → ∑ i ∈ t, w i < 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ (convexHull R) s
-- Std.Http.Data.Headers.Value
/-- Performs a case-insensitive comparison between a `Value` and a `String`. Returns `true` if they match.
 -/
Std.Http.Header.Value.is : Std.Http.Header.Value → String → Bool
-- Mathlib.Probability.CDF
/-- The cdf is non-negative.  -/
ProbabilityTheory.cdf_nonneg : ∀ (μ : MeasureTheory.Measure ℝ) (x : ℝ), 0 ≤ ↑(ProbabilityTheory.cdf μ) x
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubAddAction.ofStabilizer.addConjMap_comp_neg_apply : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] {g : G} {a b : α} (hg : b = g +ᵥ a)
  (x : ↥(SubAddAction.ofStabilizer G a)),
  (SubAddAction.ofStabilizer.conjMap ⋯) ((SubAddAction.ofStabilizer.conjMap hg) x) = x
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivWithinAt.iteratedFDerivWithin_cons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F}
  {x v w : E} {hf : IsSymmSndFDerivWithinAt 𝕜 f s x},
  UniqueDiffOn 𝕜 s → x ∈ s → (iteratedFDerivWithin 𝕜 2 f s x) ![v, w] = (iteratedFDerivWithin 𝕜 2 f s x) ![w, v]
-- Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum
/-- If a series is converging in `L^p`, then it also converges pointwise almost everywhere.  -/
MeasureTheory.Lp.hasSum_coeFn_tsum : ∀ {X : Type u_1} {E : Type u_2} {x : MeasurableSpace X} {μ : MeasureTheory.Measure X} [inst : NormedAddCommGroup E]
  {p : ENNReal} [hp : Fact (1 ≤ p)] {ι : Type u_3} [Countable ι] [CompleteSpace E] {f : ι → ↥(MeasureTheory.Lp E p μ)},
  ∑' (n : ι), ‖f n‖ₑ ≠ ⊤ → ∀ᵐ (a : X) ∂μ, HasSum (fun n => ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)
-- Lean.Meta.Tactic.Apply
Lean.Meta.getExpectedNumArgs : Lean.Expr → Lean.MetaM ℕ
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.isoApp_symm : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  (f : X ≅ Y) (i : I), CategoryTheory.Pi.isoApp f.symm i = (CategoryTheory.Pi.isoApp f i).symm
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphismClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : FunLike F α β] [toRelHomClass : RelHomClass F (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2],
  (∀ (f : F) ⦃a : α⦄ ⦃b : β⦄, f a ≤ b → ∃ c, a ≤ c ∧ f c = b) → PseudoEpimorphismClass F α β
-- Mathlib.Algebra.Ring.Pi
Pi.hasDistribNeg : {I : Type u} →
  {f : I → Type v} → [inst : (i : I) → Mul (f i)] → [(i : I) → HasDistribNeg (f i)] → HasDistribNeg ((i : I) → f i)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry!.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (size : ℕ) (k : α) (v : β)
  (r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.minEntry!
      (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) =
    (k, v)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF →
    ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = false → Std.DTreeMap.Internal.Impl.Const.get! t a = default
-- Std.Http.Protocol.H1
/-- Applies an update function to the reader sub-state while preserving all other
machine fields.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.modifyReader : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir →
    (Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir) → Std.Http.Protocol.H1.Machine dir
-- Lean.Util.SCC
_private.Lean.Util.SCC.0.Lean.SCC.getDataOf : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → α → Lean.SCC.M α Lean.SCC.Data
-- Mathlib.Order.Defs.PartialOrder
instTransGT : {α : Type u_1} → [inst : Preorder α] → Trans GT.gt GT.gt GT.gt
-- Lean.Parser.Extension
Lean.Parser.isParserAlias : Lean.Name → IO Bool
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.sup : ℝ → ℝ → ℝ
-- Mathlib.RingTheory.Ideal.Maps
Module.annihilator_eq_top_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.annihilator R M = ⊤ ↔ Subsingleton M
-- Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Polynomial.Bivariate.Transcendental.algEquivAdjoin.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A}
  (hx : Transcendental R x),
  Polynomial.Bivariate.Transcendental.algEquivAdjoin hx = Polynomial.Bivariate.Transcendental.algEquivAdjoin hx
-- Init.Grind.Lemmas
Lean.Grind.decide_eq_true : ∀ {p : Prop} {x : Decidable p}, p = True → decide p = true
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.comap_subtype_le_iff : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q r : Submodule R M}, Submodule.comap p.subtype q ≤ Submodule.comap p.subtype r ↔ p ⊓ q ≤ p ⊓ r
-- Init.Data.Int.Basic
/-- For all natural numbers `n`, `Int.ofNat n` is non-negative.
 -/
Int.NonNeg.mk : ∀ (n : ℕ), (Int.ofNat n).NonNeg
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_fun_eq_zero_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R}, x.coeff = 0 ↔ x = 0
-- Lean.Elab.Tactic.Simp
/-- Construct a `Simp.DischargeWrapper` from the `Syntax` for a `simp` discharger.  -/
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.mkDischargeWrapper : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.Simp.DischargeWrapper
-- Std.Data.HashMap.Lemmas
Std.HashMap.filterMap_equiv_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ}, (Std.HashMap.filterMap (fun k v => some (f k v)) m).Equiv (Std.HashMap.map f m)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.restrictionLT_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J] {j : J}
  (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {i : J} (hi : i ≤ j) {k₁ k₂ : ↑(Set.Iio i)} (φ : k₁ ⟶ k₂),
  (CategoryTheory.SmallObject.restrictionLT F hi).map φ = F.map (CategoryTheory.homOfLE ⋯)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.vComp_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.LaxTrans F G)
  (θ : CategoryTheory.Oplax.LaxTrans G H) (a : B),
  CategoryTheory.CategoryStruct.comp (η.vCompNaturality θ (CategoryTheory.CategoryStruct.id a))
      (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.vCompApp θ a)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.vCompApp θ a) (H.mapId a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (η.vCompApp θ a)).hom
        (CategoryTheory.Bicategory.leftUnitor (η.vCompApp θ a)).inv)
-- Std.Http.Internal.IndexMultiMap
/-- Checks if the key-value pair is present in the map.
 -/
Std.Internal.IndexMultiMap.hasEntry : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → [BEq β] → α → β → Bool
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
_private.Mathlib.LinearAlgebra.Matrix.ToLinearEquiv.0.Matrix.exists_mulVec_eq_zero_iff' : ∀ {n : Type u_1} [inst : Fintype n] {A : Type u_4} (K : Type u_5) [inst_1 : DecidableEq n] [inst_2 : CommRing A]
  [Nontrivial A] [inst_4 : Field K] [inst_5 : Algebra A K] [IsFractionRing A K] {M : Matrix n n A},
  (∃ v, v ≠ 0 ∧ M.mulVec v = 0) ↔ M.det = 0
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsCircuit.contract_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {K C : Set α}, M.IsCircuit K → C ⊂ K → (M.contract C).IsCircuit (K \ C)
-- Mathlib.Data.Rat.Floor
Rat.floor_intCast_div_natCast : ∀ (n : ℤ) (d : ℕ), ⌊↑n / ↑d⌋ = n / ↑d
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.folder : Lean.Lsp.CompletionItemKind
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_pure_bot : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Filter.TendstoIxxClass Set.Ioc (pure a) ⊥
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_not_contains : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueCastD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback =
      if l₂.contains k = true then fallback else Std.Internal.List.getValueCastD k l₁ fallback
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCongrLeft_apply : ∀ {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] [inst_1 : Semiring 𝕜]
  {ι' : Type u_5} [inst_2 : Fintype ι'] {E : Type u_6} [inst_3 : SeminormedAddCommGroup E] [inst_4 : Module 𝕜 E]
  (e : ι ≃ ι') (v : PiLp p fun x => E),
  ((LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) v).ofLp = (Equiv.piCongrLeft' (fun x => E) e) v.ofLp
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sub_leadingTerm_lt_degree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f : MvPolynomial σ R},
  m.degree f ≠ 0 → m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.isQuotient_explicitCokernelπ : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y), (SemiNormedGrp.Hom.hom (SemiNormedGrp.explicitCokernelπ f)).IsQuotient
-- Mathlib.Algebra.Order.GroupWithZero.Basic
MulPosStrictMono.toMulPosMono : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : PartialOrder α] [MulPosStrictMono α], MulPosMono α
-- Lean.Elab.Tactic.Grind.Annotated
_private.Lean.Elab.Tactic.Grind.Annotated.0.Lean.Elab.Tactic.Grind.elabGrindAnnotated : Lean.Elab.Command.CommandElab
-- Mathlib.Data.Set.NAry
Set.image2_insert_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {b : β},
  Set.image2 f s (insert b t) = (fun a => f a b) '' s ∪ Set.image2 f s t
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.arcosh_pos : ∀ {x : ℝ}, 1 < x → 0 < Real.arcosh x
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteDistribLattice.MinimalAxioms.mk : ∀ {α : Type u} [inst : CompleteLattice α],
  Order.Frame.MinimalAxioms α → Order.Coframe.MinimalAxioms α → CompleteDistribLattice.MinimalAxioms α
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuationSubring_valuation : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A.valuation.valuationSubring = A
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.coroot'_apply_apply_mem_of_mem_span : ∀ {ι : Type u_1} {R : Type u_2} {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] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S M] [IsScalarTower S R M] [P.IsValuedIn S] {x : M},
  x ∈ Submodule.span S (Set.range ⇑P.root) → ∀ (i : ι), (P.coroot' i) x ∈ Set.range ⇑(algebraMap S R)
-- Mathlib.Logic.Function.Basic
Function.comp_update : ∀ {α : Sort u} [inst : DecidableEq α] {α' : Sort u_1} {β : Sort u_2} (f : α' → β) (g : α → α') (i : α) (v : α'),
  f ∘ Function.update g i v = Function.update (f ∘ g) i (f v)
-- Mathlib.Data.ENat.Basic
/-- A version of `ENat.map` for `MonoidWithZeroHom`s.  -/
MonoidWithZeroHom.ENatMap : {S : Type u_2} →
  [inst : MulZeroOneClass S] →
    [inst_1 : DecidableEq S] → [inst_2 : Nontrivial S] → (f : ℕ →*₀ S) → Function.Injective ⇑f → ℕ∞ →*₀ WithTop S
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- **Alias** of `ModelWithCorners.extendCoordChange_source_mem_nhdsWithin`. -/
OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} {x : E},
  x ∈ (ModelWithCorners.extendCoordChange e e').source →
    (ModelWithCorners.extendCoordChange e e').source ∈ nhdsWithin x (Set.range ↑I)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.isCoatom_comap_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂},
  Function.Surjective ⇑f → ∀ {p : Submodule R₂ M₂}, IsCoatom (Submodule.comap f p) ↔ IsCoatom p
-- Aesop.Util.UnorderedArraySet
_private.Aesop.Util.UnorderedArraySet.0.Aesop.UnorderedArraySet.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : SizeOf α] (rep : Array α), sizeOf { rep := rep } = 1 + sizeOf rep
-- Init.Data.Order.Classes
Std.LawfulOrderInf.le_min_iff : ∀ {α : Type u} {inst : Min α} {inst_1 : LE α} [self : Std.LawfulOrderInf α] (a b c : α), a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c