mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.μ_natural : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))
      (CategoryTheory.Functor.LaxMonoidal.μ F Y Y') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X')
      (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- Constructor for `CofibrantObject C`.  -/
HomotopicalAlgebra.CofibrantObject.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        (X : C) → [HomotopicalAlgebra.IsCofibrant X] → HomotopicalAlgebra.CofibrantObject C
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- Constructor for natural isomorphisms between cospans.  -/
CategoryTheory.Limits.cospanIsoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} →
      (z : F.obj CategoryTheory.Limits.WalkingCospan.one ≅ G.obj CategoryTheory.Limits.WalkingCospan.one) →
        (l : F.obj CategoryTheory.Limits.WalkingCospan.left ≅ G.obj CategoryTheory.Limits.WalkingCospan.left) →
          (r : F.obj CategoryTheory.Limits.WalkingCospan.right ≅ G.obj CategoryTheory.Limits.WalkingCospan.right) →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z.hom =
                  CategoryTheory.CategoryStruct.comp l.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl))
                CategoryTheory.Limits.cospanIsoMk._auto_1 →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z.hom =
                    CategoryTheory.CategoryStruct.comp r.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr))
                  CategoryTheory.Limits.cospanIsoMk._auto_3 →
                (F ≅ G)
-- Std.Data.HashMap.RawLemmas
/-- Simpler variant of `getElem?_filterMap` when `LawfulBEq` is available.  -/
Std.HashMap.Raw.getElem?_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [LawfulBEq α]
  {f : α → β → Option γ} {k : α}, m.WF → (Std.HashMap.Raw.filterMap f m)[k]? = m[k]?.bind fun x => f k x
-- Init.Classical
Classical.typeDecidable : (α : Sort u) → α ⊕' ∀ (a : α), False
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.of_le_left : ∀ {α : Type u_1} {a b a' : α} [inst : LE α], a ≤ b → a = a' → a' ≤ b
-- Mathlib.Order.SuccPred.Tree
SubRootedTree.ext : ∀ {t : RootedTree} {v₁ v₂ : SubRootedTree t}, v₁.root = v₂.root → v₁ = v₂
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.Hopf.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (X : C) → [hopf : CategoryTheory.HopfObj X] → CategoryTheory.Hopf C
-- Mathlib.Topology.Compactness.Lindelof
Set.Countable.isLindelof_sUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {S : Set (Set X)}, S.Countable → (∀ s ∈ S, IsLindelof s) → IsLindelof (⋃₀ S)
-- Mathlib.Algebra.Group.Action.Prod
Prod.mulAction.eq_1 : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α] [inst_2 : MulAction M β],
  Prod.mulAction = { toSMul := Prod.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.instFullArrowQuotient : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V],
  (CategoryTheory.Preadditive.RightFreyd.quotient V).Full
-- Std.Http.Data.Method
/-- Undo a previous checkout of a version-controlled resource.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-4.5
 -/
Std.Http.Method.uncheckout : Std.Http.Method
-- Mathlib.Algebra.MvPolynomial.Rename
/-- Every polynomial is a polynomial in finitely many variables.  -/
MvPolynomial.exists_finset_rename : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p : MvPolynomial σ R),
  ∃ s q, p = (MvPolynomial.rename Subtype.val) q
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- Given a well-ordered type `J`, a morphism `f : X ⟶ Y` in a category `C`
is a transfinite composition of shape `J` if we have a well order continuous
functor `F : J ⥤ C`, an isomorphism `F.obj ⊥ ≅ X`, a colimit cocone for `F`
whose point is `Y`, such that the composition `X ⟶ F.obj ⊥ ⟶ Y` is `f`.  -/
CategoryTheory.TransfiniteCompositionOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : Type w) →
      [inst_1 : LinearOrder J] →
        [OrderBot J] → {X Y : C} → (X ⟶ Y) → [SuccOrder J] → [WellFoundedLT J] → Type (max (max u v) w)
-- Mathlib.Topology.MetricSpace.BundledFun
/-- The underlying binary function mapping into a linearly ordered additive monoid.  -/
PseudoMetric.toFun : {X : Type u_1} → {R : Type u_2} → [inst : Zero R] → [inst_1 : Add R] → [inst_2 : LE R] → PseudoMetric X R → X → X → R
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
groupCohomology.δ₀_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (z : ↥X.X₃.ρ.invariants) (y : ↑X.X₂),
  (Rep.Hom.hom X.g) y = ↑z →
    ∀ (x : G → ↑X.X₁)
      (hx : ⇑(Rep.Hom.hom X.f) ∘ x = (CategoryTheory.ConcreteCategory.hom (groupCohomology.d₀₁ X.X₂)) y),
      (CategoryTheory.ConcreteCategory.hom (groupCohomology.δ hX 0 1 ⋯))
          ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H0Iso X.X₃).inv) z) =
        (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π X.X₁)) ⟨x, ⋯⟩
-- Mathlib.Topology.Algebra.StarSubalgebra
Subalgebra.topologicalClosure_star_comm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  [inst_7 : IsSemitopologicalSemiring A] [ContinuousStar A] (s : Subalgebra R A),
  (star s).topologicalClosure = star s.topologicalClosure
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- Every linear isometry equivalence is a measurable equivalence.  -/
LinearIsometryEquiv.toMeasurableEquiv : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup F] →
      [inst_1 : InnerProductSpace ℝ F] →
        [inst_2 : NormedAddCommGroup E] →
          [inst_3 : InnerProductSpace ℝ E] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] → [inst_6 : MeasurableSpace F] → [BorelSpace F] → (E ≃ₗᵢ[ℝ] F) → E ≃ᵐ F
-- Aesop.Tree.TreeM
Aesop.TreeM.State.mk : Aesop.Tree → Aesop.TreeM.State
-- Std.Data.DTreeMap.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DTreeMap.getKey : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap α β cmp) → (a : α) → a ∈ t → α
-- Mathlib.GroupTheory.HNNExtension
/-- The empty reduced word.  -/
HNNExtension.NormalWord.ReducedWord.empty : (G : Type u_1) → [inst : Group G] → (A B : Subgroup G) → HNNExtension.NormalWord.ReducedWord G A B
-- Mathlib.Order.RelClasses
instIsNonstrictStrictOrderLeLt : ∀ {α : Type u} [inst : Preorder α], IsNonstrictStrictOrder α (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 < x2
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.agmSequences_snd_antitone : ∀ {x y : NNReal}, Antitone fun n => (x.agmSequences y n).2
-- Init.Data.List.MapIdx
List.mapIdx_set : ∀ {α : Type u_1} {α_1 : Type u_2} {f : ℕ → α → α_1} {l : List α} {i : ℕ} {a : α},
  List.mapIdx f (l.set i a) = (List.mapIdx f l).set i (f i a)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMap'_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData),
  CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h h =
    CategoryTheory.CategoryStruct.id h.H
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Producer : Type
-- Lean.Parser.Command
Lean.Parser.Command.extends : Lean.Parser.Parser
-- Std.Data.HashSet.Raw
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.HashSet.Raw.all : {α : Type u} → Std.HashSet.Raw α → (α → Bool) → Bool
-- Init.Grind.Module.Envelope
_private.Init.Grind.Module.Envelope.0.Lean.Grind.IntModule.OfNatModule.r.match_1.eq_1 : ∀ (α : Type u_1) (motive : α × α → α × α → Sort u_2) (a b c d : α) (h_1 : (a b c d : α) → motive (a, b) (c, d)),
  (match (a, b), (c, d) with
    | (a, b), (c, d) => h_1 a b c d) =
    h_1 a b c d
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z}, IsHomeomorph g → IsHomeomorph f → IsHomeomorph (g ∘ f)
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1IsBoundedSMul : ∀ {S : Type u_2} {R : Type u_3} {M : Type u_4} [inst : SeminormedCommRing S] [inst_1 : SeminormedRing R]
  [inst_2 : SeminormedAddCommGroup M] [inst_3 : Algebra S R] [inst_4 : Module S M] [IsBoundedSMul S R]
  [IsBoundedSMul S M] [inst_7 : Module R M] [inst_8 : IsBoundedSMul R M] [inst_9 : Module Rᵐᵒᵖ M]
  [inst_10 : IsBoundedSMul Rᵐᵒᵖ M] [inst_11 : SMulCommClass R Rᵐᵒᵖ M], IsBoundedSMul S (TrivSqZeroExt R M)
-- Batteries.Data.Array.Scan
List.toArray_scanlM : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] [LawfulMonad m] {f : β → α → m β}
  {as : List α}, List.toArray <$> List.scanlM f init as = Array.scanlM f init as.toArray
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limit_map_limitObjIsoLimitCompEvaluation_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {i j : K} (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit F).map f)
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F j).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F i).hom
      (CategoryTheory.Limits.limMap (F.whiskerLeft ((CategoryTheory.evaluation K C).map f)))
-- Mathlib.Order.Directed
/-- **Alias** of the reverse direction of `directedOn_range`. -/
Directed.directedOn_range : ∀ {α : Type u_1} {ι : Sort u_3} {r : α → α → Prop} {f : ι → α}, Directed r f → DirectedOn r (Set.range f)
-- Init.Data.Vector.Basic
/-- Check if there is an element which satisfies `a == ·`.  -/
Vector.contains : {α : Type u_1} → {n : ℕ} → [BEq α] → Vector α n → α → Bool
-- Mathlib.Analysis.Convex.Segment
openSegment_eq_Ioo : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜},
  x < y → openSegment 𝕜 x y = Set.Ioo x y
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableAt.mfderiv : ∀ {𝕜 : 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'} {x : M},
  MDiffAt f x → mfderiv% f x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (Set.range ↑I) (↑(extChartAt I x) x)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.iterFromIdxM_toArray : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ},
  xs.toArray.iterFromIdxM m pos = xs.iterFromIdxM m pos
-- Mathlib.Data.Ordmap.Invariants
Ordnode.emem_iff_mem_toList : ∀ {α : Type u_1} {x : α} {t : Ordnode α}, Ordnode.Emem x t ↔ x ∈ t.toList
-- Mathlib.Data.Matrix.Basis
/-- Families of linear maps acting on each element are equivalent to linear maps from a matrix.

This can be thought of as the matrix version of `LinearMap.lsum`.  -/
Matrix.liftLinear : {m : Type u_2} →
  {n : Type u_3} →
    {R : Type u_5} →
      (S : Type u_6) →
        {α : Type u_7} →
          {β : Type u_8} →
            [DecidableEq m] →
              [DecidableEq n] →
                [Fintype m] →
                  [Fintype n] →
                    [inst : Semiring R] →
                      [inst_1 : Semiring S] →
                        [inst_2 : AddCommMonoid α] →
                          [inst_3 : AddCommMonoid β] →
                            [inst_4 : Module R α] →
                              [inst_5 : Module R β] →
                                [inst_6 : Module S β] →
                                  [inst_7 : SMulCommClass R S β] → (m → n → α →ₗ[R] β) ≃ₗ[S] Matrix m n α →ₗ[R] β
-- Mathlib.CategoryTheory.Sites.Pullback
CategoryTheory.Functor.sheafPullbackConstruction.instPreservesFiniteLimitsSheafSheafPullback : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  (G : CategoryTheory.Functor C D) (A : Type u₁) [inst_2 : CategoryTheory.Category.{v₁, u₁} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  [inst_3 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] [inst_4 : CategoryTheory.HasSheafify K A]
  [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.PreservesFiniteLimits G.op.lan],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.Functor.sheafPullbackConstruction.sheafPullback G A J K)
-- Init.Data.SInt.Basic
/-- The number of distinct values representable by `Int16`, that is, `2^16 = 65536`.  -/
Int16.size : ℕ
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_id_right_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
        (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv) h))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_of_lt_mul_right₀ : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosReflectLT α],
  0 ≤ b → b < a * b → 1 < a
-- Init.Data.Nat.Div.Lemmas
Nat.div_mul_self_eq_mod_sub_self : ∀ {x k : ℕ}, x / k * k = x - x % k
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.precomp_map_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} D]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D (Type w)) {X Y : (F.comp G).Elements} (f : X ⟶ Y),
  ↑((CategoryTheory.Functor.Elements.precomp F G).map f) = F.map ↑f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_insertIfNew : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (h : m.WF) {k a : α} {v : β k} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.get a ⋯
-- Init.Data.SInt.Lemmas
ISize.toInt_mul : ∀ (a b : ISize), (a * b).toInt = (a.toInt * b.toInt).bmod (2 ^ System.Platform.numBits)
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.two_le : ∀ {p : ℕ}, Nat.Prime p → 2 ≤ p
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  (X.cokernelSequenceCycles f g fg h n).g = X.toCycles f g fg h n
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.natTransP_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q : ℕ)
  (x : CategoryTheory.SimplicialObject C), (AlgebraicTopology.DoldKan.natTransP q).app x = AlgebraicTopology.DoldKan.P q
-- Init.Data.Vector.Count
Vector.count_pos_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α} {xs : Vector α n}, 0 < Vector.count a xs ↔ a ∈ xs
-- Mathlib.RingTheory.Localization.Basic
/-- The localization of a singleton is a singleton. Cannot be an instance due to metavariables.  -/
IsLocalization.unique : (R : Type u_4) →
  (Rₘ : Type u_5) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring Rₘ] →
        (M : Submonoid R) → [Subsingleton R] → [inst_3 : Algebra R Rₘ] → [IsLocalization M Rₘ] → Unique Rₘ
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.fintype : {C : Type u₁} → (self : CategoryTheory.Mat_ C) → Fintype self.ι
-- Lean.Parser.Do
Lean.Parser.Term.doFor.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
UpperHalfPlane.instFaithfulSMulProjGenLinGroupFinOfNatNatReal : FaithfulSMul (Matrix.ProjGenLinGroup (Fin 2) ℝ) UpperHalfPlane
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.Vec.prim : ∀ {n m : ℕ} {f : List.Vector ℕ n → List.Vector ℕ m}, Nat.Primrec'.Vec f → Nat.Partrec'.Vec f
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.free_iff_set : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.Free R M ↔ ∃ S, Nonempty (Module.Basis (↑S) R M)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.toArg : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Lean.Compiler.LCNF.Arg pu
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.instCharacteristicUpperCentralSeriesStep : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [inst_1 : N.Normal] [N.Characteristic],
  N.upperCentralSeriesStep.Characteristic
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
/-- `SymmetricAlgebra R M` is free when `M` is.  -/
SymmetricAlgebra.instModuleFree : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M], Module.Free R (SymmetricAlgebra R M)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.IterM.step_append.match_1.eq_3 : ∀ {α₁ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (h : it₁.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.done, h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_3 h
-- Mathlib.Order.Filter.NAry
Filter.map₂_bot_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {g : Filter β}, Filter.map₂ m ⊥ g = ⊥
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.congrTheorem.inj : ∀ {thm thm_1 : Lean.Meta.CongrTheorem},
  Lean.Meta.Sym.CongrInfo.congrTheorem thm = Lean.Meta.Sym.CongrInfo.congrTheorem thm_1 → thm = thm_1
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.canLift : ∀ {X : Type u_1} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : NormedRing R] [CompleteSpace R],
  CanLift C(X, R) C(X, Rˣ) (fun f => { toFun := fun x => ↑(f x), continuous_toFun := ⋯ }) fun f =>
    ∀ (x : X), IsUnit (f x)
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.instModelFieldOfCharOfACF : ∀ {K : Type u_1} [inst : FirstOrder.Language.ring.Structure K] (p : ℕ) [h : K ⊨ FirstOrder.Language.Theory.ACF p],
  K ⊨ FirstOrder.Language.Theory.fieldOfChar p
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.instCoeSubmodule : {R : Type u_1} →
  {E : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommMonoid E] → [inst_4 : Module R E] → Coe (Submodule R E) (PointedCone R E)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.SeparatingRight.toBilin : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {M : Matrix ι ι R₂},
  M.SeparatingRight → ∀ (b : Module.Basis ι R₂ M₂), LinearMap.SeparatingRight ((Matrix.toBilin b) M)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, (∃ h, CategoryTheory.Limits.IsZero h.left.H) → S.Exact
-- Std.Http.Data.Headers
/-- Checks if a header with the given name exists.
 -/
Std.Http.Headers.contains : Std.Http.Headers → Std.Http.Header.Name → Bool
-- Lean.Elab.BuiltinTerm
_private.Lean.Elab.BuiltinTerm.0.Lean.Elab.Term.evalFilePath : Lean.Syntax → Lean.Elab.TermElabM System.FilePath
-- Mathlib.Topology.Sets.Closeds
/-- The type of closed sets is inhabited, with default element the empty set.  -/
TopologicalSpace.Closeds.instInhabited : {α : Type u_2} → [inst : TopologicalSpace α] → Inhabited (TopologicalSpace.Closeds α)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- a morphism in the family of presieves `R`  -/
CategoryTheory.Presieve.BindStruct.g : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Presieve X} →
        {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} →
          {Z : C} → {h : Z ⟶ X} → (self : S.BindStruct R h) → Z ⟶ self.Y
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSub_zero_vadd : ∀ {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M} [inst_1 : AddOreLocalization.AddOreSet S]
  [inst_2 : AddAction M X] (r : M) (x : AddOreLocalization S X), (r -ₒ 0) +ᵥ x = r +ᵥ x
-- Init.Data.Option.Lemmas
Option.map_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (o : Option α)
  (H : ∀ (a : α), o = some a → p a), Option.map g (Option.pmap f o H) = Option.pmap (fun a h => g (f a h)) o H
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.instMembershipSet : {G : Type u} → [inst : Group G] → Membership (Set G) (GroupFilterBasis G)
-- Lean.Server.Requests
Lean.Server.RequestContext.initParams : Lean.Server.RequestContext → Lean.Lsp.InitializeParams
-- Lean.Expr
Lean.Expr.lam.sizeOf_spec : ∀ (binderName : Lean.Name) (binderType body : Lean.Expr) (binderInfo : Lean.BinderInfo),
  sizeOf (Lean.Expr.lam binderName binderType body binderInfo) =
    1 + sizeOf binderName + sizeOf binderType + sizeOf body + sizeOf binderInfo