mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.containsKey_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] (k k' : α) (f : β → β) (l : List ((_ : α) × β)),
  Std.Internal.List.containsKey k' (Std.Internal.List.Const.modifyKey k f l) = Std.Internal.List.containsKey k' l
-- Mathlib.GroupTheory.Nilpotent
/-- Products of nilpotent groups are nilpotent if their nilpotency class is bounded.  -/
Group.isNilpotent_pi_of_bounded_class : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [∀ (i : η), Group.IsNilpotent (Gs i)] (n : ℕ),
  (∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n) → Group.IsNilpotent ((i : η) → Gs i)
-- Lean.Linter.Init
/-- Tag attached by `logLint` to every linter warning so consumers
(e.g. `Lean.Linter.recordLints`) can distinguish linter-produced messages
from other tagged messages such as named errors or unknown-identifier messages.
 -/
Lean.Linter.linterMessageTag : Lean.Name
-- Init.System.Uri
/-- Convert the given uri to a FilePath stripping the 'file://' prefix,
ignoring the optional host name.  -/
System.Uri.fileUriToPath? : String → Option System.FilePath
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.mul_apply : ∀ (f g : CircleDeg1Lift) (x : ℝ), (f * g) x = f (g x)
-- Batteries.Data.Fin.Fold
Fin.dfoldr_zero : ∀ {α : Fin (0 + 1) → Type u_1} (f : (i : Fin 0) → α i.succ → α i.castSucc) (x : α (Fin.last 0)), Fin.dfoldr 0 α f x = x
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.Subgraph.isAcyclic_coe_bot : ∀ {V : Type u_1} (G : SimpleGraph V), ⊥.coe.IsAcyclic
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_const_mul_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_6}
  [inst_1 : NormedDivisionRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] (c : 𝕜') (f : 𝕜 → 𝕜'),
  iteratedDerivWithin n (fun z => c * f z) s x = c * iteratedDerivWithin n f s x
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- The value depends only on the residue class of `a` mod `b`.  -/
Mathlib.Meta.NormNum.JacobiSym.mod_left : ∀ (a : ℤ) (b ab' : ℕ) (ab r b' : ℤ),
  ↑b = b' → a % b' = ab → ↑ab' = ab → Mathlib.Meta.NormNum.jacobiSymNat ab' b = r → jacobiSym a b = r
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.add_apply : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] (g₁ g₂ : DirectSum ι fun i => β i) (i : ι),
  (g₁ + g₂) i = g₁ i + g₂ i
-- Init.Data.Vector.Attach
Vector.map_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {p : α → Prop} {g : β → γ} {f : (a : α) → p a → β}
  {xs : Vector α n} (H : ∀ a ∈ xs, p a), Vector.map g (Vector.pmap f xs H) = Vector.pmap (fun a h => g (f a h)) xs H
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
TensorProduct.map_surjective : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : Module R N] [inst_4 : Module R P] {g : N →ₗ[R] P},
  Function.Surjective ⇑g →
    ∀ {N' : Type u_6} {P' : Type u_7} [inst_5 : AddCommMonoid N'] [inst_6 : AddCommMonoid P'] [inst_7 : Module R N']
      [inst_8 : Module R P'] {g' : N' →ₗ[R] P'}, Function.Surjective ⇑g' → Function.Surjective ⇑(TensorProduct.map g g')
-- Init.Meta.Defs
/-- Creates literal syntax for a natural number.

If `info` is provided, then the literal's source information is copied from it.
 -/
Lean.Syntax.mkNatLit : ℕ → optParam Lean.SourceInfo Lean.SourceInfo.none → Lean.NumLit
-- Mathlib.FieldTheory.Differential.Basic
Differential.logDeriv_one : ∀ {R : Type u_1} [inst : Field R] [inst_1 : Differential R], Differential.logDeriv 1 = 0
-- Mathlib.Data.Set.Lattice
Set.subset_iInter₂ : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), s ⊆ t i j) → s ⊆ ⋂ i, ⋂ j, t i j
-- Mathlib.Algebra.Lie.Prod
/-- The left injection into a product is a Lie algebra map.  -/
LieHom.inl : (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₂] → L₁ →ₗ⁅R⁆ L₁ × L₂
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_smul_vsub_vadd_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {p₁ p₂ : P} (x : P), p₁ ∈ s → p₂ ∈ s → ∀ {t : R}, 0 ≤ t → s.WSameSide x (t • (x -ᵥ p₁) +ᵥ p₂)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (m.insertMany l).getD k fallback = m.getD k fallback
-- Mathlib.Order.KrullDimension
Order.height_le : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞},
  (∀ (p : LTSeries α), RelSeries.last p = a → ↑p.length ≤ n) → Order.height a ≤ n
-- Mathlib.GroupTheory.Complement
/-- A right transversal can be viewed as a function mapping each element of the group
to the chosen representative from that right coset.  -/
Subgroup.IsComplement.toRightFun : {G : Type u_1} → [inst : Group G] → {H : Subgroup G} → {T : Set G} → Subgroup.IsComplement (↑H) T → G → ↑T
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.mk.injEq : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (χ_ne : χ ≠ 1) (χ_sq : χ ^ 2 = 1)
  (hχ : DirichletCharacter.LFunction χ 1 = 0) (χ_1 : DirichletCharacter ℂ N) (χ_ne_1 : χ_1 ≠ 1) (χ_sq_1 : χ_1 ^ 2 = 1)
  (hχ_1 : DirichletCharacter.LFunction χ_1 1 = 0),
  ({ χ := χ, χ_ne := χ_ne, χ_sq := χ_sq, hχ := hχ } = { χ := χ_1, χ_ne := χ_ne_1, χ_sq := χ_sq_1, hχ := hχ_1 }) =
    (χ = χ_1)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.interpolate_eq_of_values_eq_on : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r r' : ι → F),
  (∀ i ∈ s, r i = r' i) → (Lagrange.interpolate s v) r = (Lagrange.interpolate s v) r'
-- Mathlib.Topology.Algebra.Module.PerfectSpace
perfectSpace_of_module : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [Nontrivial E] [inst_4 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E], PerfectSpace E
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.le.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α}, AddLocalization.le = { le := fun a b => a.liftOn₂ b (fun a₁ a₂ b₁ b₂ => ↑b₂ + a₁ ≤ ↑a₂ + b₁) ⋯ }
-- Batteries.Data.String.Lemmas
String.mk_length : ∀ (s : List Char), (String.ofList s).length = s.length
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The equivalence between `coind₁` and `coind` of the trivial representation of trivial
subgroup of `G`.  -/
ContRepresentation.coind₁Equivcoind : {R : Type u_1} →
  {V : Type u_3} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : IsTopologicalAddGroup V] →
            [inst_4 : Module R V] →
              {G : Type u_7} →
                [inst_5 : Group G] →
                  [inst_6 : TopologicalSpace G] →
                    [inst_7 : TopologicalSpace R] →
                      [inst_8 : ContinuousSMul R V] →
                        [inst_9 : IsTopologicalGroup G] →
                          (ContRepresentation.trivial R (↥⊥) V).coind₁.Equiv
                            (ContRepresentation.coind 1 (ContRepresentation.trivial R G V))
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- The exact formula for the number of edges in `turanGraph n r`.  -/
SimpleGraph.card_edgeFinset_turanGraph : ∀ {n r : ℕ}, (SimpleGraph.turanGraph n r).edgeFinset.card = (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) + (n % r).choose 2
-- Mathlib.RingTheory.Morita.Matrix
toModuleCatFromModuleCatLinearEquiv.eq_1 : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (M : ModuleCat (Matrix ι ι R))
  (j : ι),
  toModuleCatFromModuleCatLinearEquiv R M j =
    { toFun := fun m i => ⟨Matrix.single j i 1 • m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯,
      invFun := fun m => ∑ i, Matrix.single i j 1 • ↑(m i), left_inv := ⋯, right_inv := ⋯ }
-- Lean.Meta.Tactic.Grind.Types
/-- Split diagnostic information. This information is only collected when `set_option diagnostics true`  -/
Lean.Meta.Grind.State.splitDiags : Lean.Meta.Grind.State → Lean.PArray Lean.Meta.Grind.SplitDiagInfo
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- For natural numbers `n`, the logarithmic counting function for the zeros of `f ^ n` equals `n`
times the logarithmic counting function for the zeros of `f`.
 -/
ValueDistribution.logCounting_pow_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {f : 𝕜 → 𝕜} {n : ℕ},
  Meromorphic f → ValueDistribution.logCounting (f ^ n) 0 = n • ValueDistribution.logCounting f 0
-- Mathlib.Data.Set.Operations
Set.mem_sdiff : ∀ {α : Type u} {s t : Set α} (x : α), x ∈ s \ t ↔ x ∈ s ∧ x ∉ t
-- Mathlib.Algebra.Order.Sub.WithTop
/-- If `α` has a subtraction and a bottom element, we can extend the subtraction to `WithTop α`, by
setting `x - ⊤ = ⊥` and `⊤ - x = ⊤`.  -/
WithTop.sub : {α : Type u_1} → [Sub α] → [Bot α] → WithTop α → WithTop α → WithTop α
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_dvd_lcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c d : α}, a ∣ b → c ∣ d → lcm a c ∣ lcm b d
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.one_le_ofNat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ} [inst_5 : n.AtLeastTwo], 1 ≤ OfNat.ofNat n
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_injective_of_surjective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂}, Function.Surjective ⇑f → Function.Injective (Submodule.comap f)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balRight.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (l : RBTree.RBNode α) →
      ((a : RBTree.RBNode α) →
          (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b)) →
        ((a : RBTree.RBNode α) →
            (x : α) →
              (b : RBTree.RBNode α) →
                (y : α) →
                  (c : RBTree.RBNode α) →
                    motive
                      (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c))) →
          ((l : RBTree.RBNode α) →
              (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                  l = RBTree.RBNode.node RBTree.RBColor.black a x b → False) →
                (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
                    l = RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) →
                      False) →
                  motive l) →
            motive l
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Iso.conj_eq_conj : ∀ {S : Type u} [inst : CommSemiring S] {X X' : SemimoduleCat S} (i : X ≅ X') (f : CategoryTheory.End X),
  i.conj f = { hom' := i.toLinearEquivₛ.conj (SemimoduleCat.Hom.hom f) }
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `M'` is the localization of `M` at `S` and `A = S⁻¹R`, then `M'` is an `A`-module.  -/
IsLocalizedModule.module : {R : Type u_6} →
  {A : Type u_7} →
    {M : Type u_8} →
      {M' : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : Algebra R A] →
              (S : Submonoid R) →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : Module R M] →
                    [inst_5 : AddCommMonoid M'] →
                      [inst_6 : Module R M'] →
                        [IsLocalization S A] → (f : M →ₗ[R] M') → [IsLocalizedModule S f] → Module A M'
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k a : α}, (m.erase k).get? a = if (k == a) = true then none else m.get? a
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.inhabited : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → Inhabited (E →ₛₗ.[σ] F)
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.surjective_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.Surjective f ↔ Function.Surjective ⇑f
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- Given `f : X ⟶ Y` and `g : Y ⟶ Z` such that `g` is separated, the induced map
`X ⟶ X ×[Z] Y` is a closed immersion.  -/
AlgebraicGeometry.IsSeparated.instIsClosedImmersionLiftSchemeId : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X) f ⋯)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instStarAddMonoid : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : AddMonoid β] → [StarAddMonoid β] → StarAddMonoid (MeasureTheory.SimpleFunc α β)
-- Init.SimpLemmas
beq_self_eq_true' : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), (a == a) = true
-- Mathlib.Data.Finset.Lattice.Union
Finset.sup_biUnion : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : β → α} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : DecidableEq β] (s : Finset γ) (t : γ → Finset β), (s.biUnion t).sup f = s.sup fun x => (t x).sup f
-- Mathlib.RingTheory.Ideal.Colon
Ideal.le_colon : ∀ {R : Type u_1} [inst : Semiring R] {I : Ideal R} {S : Set R} [I.IsTwoSided], I ≤ Submodule.colon I S
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₁_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (X X_1 X_2 : C),
  (((CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap₁ F).app X).app X_1).app X_2 =
    F.map (CategoryTheory.MonoidalCategoryStruct.associator X X_1 X_2).hom
-- Init.Sym.Lemmas
Lean.Sym.UInt8.lt_eq_false : ∀ (a b : UInt8), decide (a < b) = false → (a < b) = False
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.strictlyPositive_le_positive : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : PartialOrder M] [inst_4 : IsOrderedAddMonoid M] [inst_5 : Module R M] [inst_6 : PosSMulStrictMono R M],
  ConvexCone.strictlyPositive R M ≤ ConvexCone.positive R M
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_Iic : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (q : ℚ),
  Rat.cast ⁻¹' Set.Iic ↑q = Set.Iic q
-- Mathlib.Algebra.Group.WithOne.Defs
_private.Mathlib.Algebra.Group.WithOne.Defs.0.WithOne.unone.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : WithOne α) → x ≠ 1 → Sort u_2) (x : α) (x_1 : ↑x ≠ 1)
  (h_1 : (x : α) → (x_2 : ↑x ≠ 1) → motive (some x) x_2),
  (match some x, x_1 with
    | some x, x_2 => h_1 x x_2) =
    h_1 x x_1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.congr_simp : ∀ {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 : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 →
    ∀ (signs signs_1 : Finset (Fin (n + 1))), signs = signs_1 → s.ExcenterExists signs = s_1.ExcenterExists signs_1
-- Mathlib.Order.Atoms
eq_sInf_coatoms : ∀ {α : Type u_4} [inst : CompleteLattice α] [IsCoatomistic α] (b : α), ∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a
-- Mathlib.Tactic.ExistsI
/-- `existsi e₁, e₂, ⋯` instantiates existential quantifiers in the main goal by using `e₁`, `e₂`, ...
as witnesses. `existsi e₁, e₂, ⋯` is equivalent to `refine ⟨e₁, e₂, ⋯, ?_⟩`.

See also `exists`: `exists e₁, e₂, ⋯` is equivalent to `existsi e₁, e₂, ⋯; try trivial`.

Examples:

```lean
example : ∃ x : Nat, x = x := by
  existsi 42
  rfl

example : ∃ x : Nat, ∃ y : Nat, x = y := by
  existsi 42, 42
  rfl
```
 -/
Mathlib.Tactic.«tacticExistsi_,,» : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr.compare : Lean.Meta.Grind.Arith.CommRing.EqCnstr → Lean.Meta.Grind.Arith.CommRing.EqCnstr → Ordering
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_5.splitter : {α₂ β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Option (Std.IterM m β) → Sort u_3) →
      (it₂ : Option (Std.IterM m β)) → (Unit → motive none) → ((it₂ : Std.IterM m β) → motive (some it₂)) → motive it₂
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The underlying `G`-equivariant linear map.  -/
TopRep.Hom.hom' : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] →
        [inst_2 : Monoid G] → {A : TopRep k G} → {B : TopRep k G} → A.Hom B → ContIntertwiningMap A.ρ B.ρ
-- Mathlib.Topology.Algebra.ConstMulAction
/-- **Alias** of the reverse direction of `vadd_mem_nhds_vadd_iff`. -/
vadd_mem_nhds_vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] {t : Set α} (g : G) {a : α}, t ∈ nhds a → g +ᵥ t ∈ nhds (g +ᵥ a)
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.coeff_inj : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W],
  Function.Injective ⇑HVertexOperator.coeff
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.run.match_1.eq_1 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (ca : Computation α) → motive (Sum.inr ca)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr ca => h_2 ca) =
    h_1 a
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- `AlternatingMap.domDomCongr` as an equivalence.

This is declared separately because it does not work with dot notation.  -/
AlternatingMap.domDomCongrEquiv : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] → {ι : Type u_7} → {ι' : Type u_8} → ι ≃ ι' → M [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp : ∀ {α : Type u_2} {β : Type u_3} {δ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → β} {g g' : β → δ},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → g =ᵐ[ν] g' → g ∘ f =ᵐ[μ] g' ∘ f
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_le_aleph0_iff : ∀ {α : Type u}, Cardinal.mk α ≤ Cardinal.aleph0 ↔ Countable α
-- Mathlib.CategoryTheory.ObjectProperty.Small
/-- A property of objects is small relative to a universe `w`
if the corresponding subtype is.  -/
CategoryTheory.ObjectProperty.Small : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.  -/
CategoryTheory.Functor.PreservesMonomorphisms.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : F.PreservesMonomorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  CategoryTheory.Mono (F.map f)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.continuous_infEDist`.

---

The edist to a set depends continuously on the point  -/
EMetric.continuous_infEdist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, Continuous fun x => Metric.infEDist x s
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.sqrt_normSq_eq_norm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F), √(InnerProductSpace.Core.normSq x) = ‖x‖
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.realSize.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.BinomialHeap.Imp.Heap α → Sort u_2) →
    (x : Batteries.BinomialHeap.Imp.Heap α) →
      (Unit → motive Batteries.BinomialHeap.Imp.Heap.nil) →
        ((rank : ℕ) →
            (val : α) →
              (c : Batteries.BinomialHeap.Imp.HeapNode α) →
                (s : Batteries.BinomialHeap.Imp.Heap α) → motive (Batteries.BinomialHeap.Imp.Heap.cons rank val c s)) →
          motive x
-- Mathlib.Combinatorics.SimpleGraph.Diam
/-- The center of a simple graph is the set of vertices with eccentricity equal to the radius.  -/
SimpleGraph.center : {α : Type u_1} → SimpleGraph α → Set α
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.builderName : Aesop.CoreRuleBuilderOutput → Aesop.BuilderName
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.symm.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S'),
  equiv.symm = { toMulEquiv := equiv.symm, inl_comm := ⋯, rightHom_comm := ⋯ }
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM.closed : Lean.Meta.TacticResultCNM
-- Mathlib.Analysis.Convex.Strong
UniformConcaveOn.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ ψ : ℝ → ℝ} {s : Set E} {f : E → ℝ},
  ψ ≤ φ → UniformConcaveOn s φ f → UniformConcaveOn s ψ f
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_nonneg : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b → (∀ u ∈ Set.Icc a b, 0 ≤ f u) → 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.exists_multiset_of_mem_closure : ∀ {M : Type u_4} [inst : CommMonoid M] {s : Set M} {x : M}, x ∈ Submonoid.closure s → ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.extend_comp_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  [CompleteSpace β] [T0Space β] {f : pkg.space → β}, UniformContinuous f → pkg.extend (f ∘ pkg.coe) = f