mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.map_comp_inrHom : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N),
  (TrivSqZeroExt.map f).toLinearMap ∘ₗ TrivSqZeroExt.inrHom R' M = TrivSqZeroExt.inrHom R' N ∘ₗ f
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDocumentHighlightParams : Lean.Lsp.FileSource Lean.Lsp.DocumentHighlightParams
-- Std.Http.Data.Response
Std.Http.Response.mk.inj : ∀ {t : Type} {line : Std.Http.Response.Head} {body : t} {extensions : Std.Http.Extensions}
  {line_1 : Std.Http.Response.Head} {body_1 : t} {extensions_1 : Std.Http.Extensions},
  { line := line, body := body, extensions := extensions } =
      { line := line_1, body := body_1, extensions := extensions_1 } →
    line = line_1 ∧ body = body_1 ∧ extensions = extensions_1
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.homMk_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} (x y : F.Elements)
  (f : x.fst ⟶ y.fst) (hf : (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = y.snd),
  ↑(CategoryTheory.CategoryOfElements.homMk x y f hf) = f
-- Lean.Server.Utils
/-- Constructs a `$/lean/fileProgress` notification marking processing as done.  -/
Lean.Server.mkFileProgressDoneNotification : Lean.Server.DocumentMeta → Lean.JsonRpc.Notification Lean.Lsp.LeanFileProgressParams
-- Mathlib.Order.Grade
/-- `grade` is strictly monotonic.  -/
GradeOrder.grade_strictMono : ∀ {𝕆 : Type u_5} {α : Type u_6} {inst : Preorder 𝕆} {inst_1 : Preorder α} [self : GradeOrder 𝕆 α],
  StrictMono GradeOrder.grade
-- Init.Grind.Config
/-- If `locals` is `true`, `grind` will add all definitions from the current file.  -/
Lean.Grind.Config.locals : Lean.Grind.Config → Bool
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.not_isUnit_iff_inverse_eq_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀] {x : M₀}, ¬IsUnit x ↔ Ring.inverse x = 0
-- Mathlib.Data.List.TakeWhile
_private.Mathlib.Data.List.TakeWhile.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.subtype_apply : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {S : L.ElementarySubstructure M} {x : ↥S},
  S.subtype x = ↑x
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.instCovariantClassHSMulLe : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M],
  CovariantClass α (Submodule R M) HSMul.hSMul LE.le
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey? k = m₁.getKey? k
-- Lean.Syntax
Lean.Syntax.instReprRange.repr : Lean.Syntax.Range → ℕ → Std.Format
-- Mathlib.Combinatorics.SimpleGraph.UniversalVerts
/-- A component of the graph with universal vertices is even if we remove a set of representatives
of odd components and a subset of universal vertices.

This is because the number of vertices in the even components is not affected, and from odd
components exactly one vertex is removed.  -/
SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_union : ∀ {V : Type u_1} {G : SimpleGraph V} {t : Set V} {s : Set ↑G.deleteUniversalVerts.verts}
  (K : G.deleteUniversalVerts.coe.ConnectedComponent),
  t ⊆ G.universalVerts →
    SimpleGraph.ConnectedComponent.Represents s G.deleteUniversalVerts.coe.oddComponents →
      Even (Subtype.val '' K.supp \ (Subtype.val '' s ∪ t)).ncard
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonResolvableCompletionList.toJson : Lean.Lsp.ResolvableCompletionList → Lean.Json
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_add_const_Ioo : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => x + a) '' Set.Ioo b c = Set.Ioo (b + a) (c + a)
-- Init.Data.List.MinMaxOn
List.max_map_eq_max : ∀ {α : Type u_1} {β : Type u_2} [inst : Max α] [inst_1 : LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α]
  [inst_4 : Max β] [inst_5 : LE β] [DecidableLE β] [Std.IsLinearPreorder β] [Std.LawfulOrderLeftLeaningMax β]
  {f : α → β}, (∀ (a b : α), f a ≤ f b ↔ a ≤ b) → ∀ {l : List α} {h : l ≠ []}, (List.map f l).max ⋯ = f (l.max h)
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.injective_isStableUnderComposition : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] x =>
    Function.Injective x).IsStableUnderComposition
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.monotoneIntro.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α} (hu : Monotone u)
  (hl : Monotone l) (h_u_l : ∀ (a : α), a ≤ u (l a)) (h_l_u : ∀ (b : β), l (u b) = b),
  GaloisInsertion.monotoneIntro hu hl h_u_l h_l_u = { choice := fun x x_1 => l x, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.flattenList.toNatAux.eq_1 : ∀ {n : ℕ}, BitVec.flattenList.toNatAux [] = 0
-- Init.Data.Array.Lemmas
List.anyM_toArray : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α},
  Array.anyM p l.toArray = List.anyM p l
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_4 : Nat.Partrec.Code.right.eval = ↑fun n => (Nat.unpair n).2
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.normal_op : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup G}, H.op.Normal ↔ H.Normal
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyAt : {s : String.Slice} → (pos : s.Pos) → pos ≠ s.endPos → String.Slice.Pattern.ForwardSliceSearcher s
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀_id_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) {a : M}
  (f : CategoryTheory.ShiftedHom X Y a),
  (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (CategoryTheory.CategoryStruct.id X)).comp f ⋯ = f
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndParamKind.target.sizeOf_spec : sizeOf Lean.Meta.FunIndParamKind.target = 1
-- Init.Simproc
_private.Init.Simproc.0.Lean.Parser.mkAttributeCmds : Lean.TSyntax `Lean.Parser.Term.attrKind →
  Option (Lean.TSyntax [`Lean.Parser.Tactic.simpPre, `Lean.Parser.Tactic.simpPost]) →
    Option (Lean.Syntax.TSepArray `ident ",") → Lean.Ident → Lean.MacroM (Array Lean.Syntax)
-- Init.Data.UInt.Lemmas
UInt64.toFin_inj : ∀ {a b : UInt64}, a.toFin = b.toFin ↔ a = b
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.Parser.getPivot : Array ℤ → Std.Sat.Literal ℕ
-- Batteries.Data.List.Basic
/-- `dropPrefix? l p` returns
`some r` if `l = p' ++ r` for some `p'` which is paiwise `==` to `p`,
and `none` otherwise.  -/
List.dropPrefix? : {α : Type u_1} → [BEq α] → List α → List α → Option (List α)
-- Mathlib.Order.KrullDimension
Order.coheight_top : ∀ (α : Type u_3) [inst : Preorder α] [inst_1 : OrderTop α], Order.coheight ⊤ = 0
-- Mathlib.Condensed.Light.InternallyProjective
/-- Given a `P : LightProfinite`, the light free light condensed module `R[P]` is internally projective
if and only if, for all `A B : LightCondMod R`, for all epimorphisms `e : A ⟶ B`, for all
`S : LightProfinite` and all morphisms `g : R[S × P] ⟶ B`, there exists a `S' : LightProfinite`
with a surjection `π : S' ⟶ S` and a morphism `g' : R[S' × P] ⟶ A`, making the diagram
```
R[S' × P] --> A
  |           |
  v           v
R[S × P]  --> B
```
commute.
 -/
LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition' : ∀ (R : Type u) [inst : CommRing R] (P : LightProfinite),
  CategoryTheory.InternallyProjective ((LightCondensed.free R).obj P.toCondensed) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite)
      (g : (LightCondensed.free R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj S P).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)),
          ∃ g',
            CategoryTheory.CategoryStruct.comp
                ((LightCondensed.free R).map
                  (lightProfiniteToLightCondSet.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight π P)))
                g =
              CategoryTheory.CategoryStruct.comp g' e
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActionResult.stuck.inj : ∀ {gs gs_1 : List Lean.Meta.Grind.Goal},
  Lean.Meta.Grind.ActionResult.stuck gs = Lean.Meta.Grind.ActionResult.stuck gs_1 → gs = gs_1
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.inter : ∀ {α : Type u_1} {s t : Set α} {P : α → Prop} [inst : LE α],
  IsRelUpperSet s P → IsRelUpperSet t P → IsRelUpperSet (s ∩ t) P
-- Mathlib.Condensed.Light.Instances
LightProfinite.hasSheafify : ∀ (A : Type u') [inst : CategoryTheory.Category.{u, u'} A] [CategoryTheory.Limits.HasLimits A]
  [CategoryTheory.Limits.HasColimits A] {FA : A → A → Type v} {CA : A → Type u}
  [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_4 : CategoryTheory.ConcreteCategory A FA]
  [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [(CategoryTheory.forget A).ReflectsIsomorphisms],
  CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) A
-- Lean.Exception
/-- Throw an error exception using the given message data.
The result of `getRef` is used as position information.
Recall that `getRef` returns the current "reference" syntax.
 -/
Lean.throwError : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → Lean.MessageData → m α
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNNRat.of_raw : ∀ (α : Type u_1) [inst : DivisionSemiring α] (n d : ℕ), ↑d ≠ 0 → Mathlib.Meta.NormNum.IsNNRat (NNRat.rawCast n d) n d
-- Mathlib.MeasureTheory.Measure.Dirac
/-- The assignment `x ↦ dirac x` is injective, assuming the measurable space separates points.  -/
MeasureTheory.injective_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSpace.SeparatesPoints α],
  Function.Injective fun x => MeasureTheory.Measure.dirac x
-- Std.Data.HashMap.Lemmas
Std.HashMap.ofArray_eq_ofList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} (a : Array (α × β)),
  Std.HashMap.ofArray a = Std.HashMap.ofList a.toList
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hurwitzOddFEPair_g₀ : ∀ (a : UnitAddCircle), (HurwitzZeta.hurwitzOddFEPair a).g₀ = 0
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
_private.Mathlib.Analysis.InnerProductSpace.Orthonormal.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
summableUniformlyOn_iff_hasSumUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α], SummableUniformlyOn f s ↔ HasSumUniformlyOn f (fun x => ∑' (i : ι), f i x) s
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the entry (key-value pair) for the key `k`, or panics if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.getEntry! : {α : Type u} →
  {β : α → Type v} → [Ord α] → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Internal.Impl α β → α → (a : α) × β a
-- Mathlib.Tactic.Ring.Common
/-- Zero is a polynomial. `e` is the expression `0`.  -/
Mathlib.Tactic.Ring.Common.ExSum.zero : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} → {sα : Q(CommSemiring «$α»)} → Mathlib.Tactic.Ring.Common.ExSum BaseType sα q(0)
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- Linear maps `(n → R) →ₗ[R] (n → R)` are algebra equivalent to `Matrix n n R`.  -/
LinearMap.toMatrixAlgEquiv' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type u_5} → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → ((n → R) →ₗ[R] n → R) ≃ₐ[R] Matrix n n R
-- Mathlib.Condensed.Functors
/-- Increase the size of the target category of condensed sets.  -/
Condensed.ulift : CategoryTheory.Functor (Condensed (Type u)) CondensedSet
-- Mathlib.Order.Types.Arithmetic
OrderType.instMonoid : Monoid OrderType.{u}
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.expr.injEq : ∀ (e e_1 : Lean.Expr),
  (Lean.Elab.Tactic.ResolveSimpIdResult.expr e = Lean.Elab.Tactic.ResolveSimpIdResult.expr e_1) = (e = e_1)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.hasColimit_multispan_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [CategoryTheory.Limits.HasMulticoequalizer D.diagram] [CategoryTheory.Limits.PreservesColimit D.diagram.multispan F],
  CategoryTheory.Limits.HasColimit (D.diagram.multispan.comp F)
-- Lean.Expr
/-- Given a sequence of nested foralls `(a₁ : α₁) → ... → (aₙ : αₙ) → _`,
returns the names `[a₁, ... aₙ]`.  -/
Lean.Expr.getForallBinderNames : Lean.Expr → List Lean.Name
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
BoundedContinuousFunction.charMonoidHom.eq_1 : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e) (hL : Continuous fun p => (L p.1) p.2),
  BoundedContinuousFunction.charMonoidHom he hL =
    { toFun := fun w => BoundedContinuousFunction.char he hL (Multiplicative.toAdd w), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor_map_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  {X Y : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X ⟶ Y),
  ↑((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).map f) = f.base
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.integral_iUnion : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {ι : Type u_7} [Countable ι] {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      μ.IntegrableOn f (⋃ i, s i) → ∫ᵛ (x : X) in ⋃ n, s n, f x ∂[B; μ] = ∑' (n : ι), ∫ᵛ (x : X) in s n, f x ∂[B; μ]
-- Mathlib.Data.List.Defs
/-- A recursor for pairs of lists. To have `C l₁ l₂` for all `l₁`, `l₂`, it suffices to have it for
`l₂ = []` and to be able to pour the elements of `l₁` into `l₂`.  -/
List.permutationsAux.rec : {α : Type u_1} →
  {C : List α → List α → Sort v} →
    ((is : List α) → C [] is) →
      ((t : α) → (ts is : List α) → C ts (t :: is) → C is [] → C (t :: ts) is) → (l₁ l₂ : List α) → C l₁ l₂
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.mop_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C), (β_ X Y).mop = β_ { unmop := Y } { unmop := X }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The linear map forgetting that a bounded continuous function is bounded.  -/
BoundedContinuousFunction.toContinuousMapLinearMap : (α : Type u) →
  (β : Type v) →
    (𝕜 : Type u_2) →
      [inst : PseudoMetricSpace 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : PseudoMetricSpace β] →
            [inst_3 : Semiring 𝕜] →
              [inst_4 : AddCommMonoid β] →
                [inst_5 : Module 𝕜 β] →
                  [inst_6 : IsBoundedSMul 𝕜 β] →
                    [inst_7 : BoundedAdd β] → [inst_8 : ContinuousAdd β] → BoundedContinuousFunction α β →ₗ[𝕜] C(α, β)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.tr.match_1.congr_eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} (motive : Option (Λ × Turing.TM0.Stmt Γ) → Sort u_3)
  (x : Option (Λ × Turing.TM0.Stmt Γ)) (h_1 : Unit → motive none)
  (h_2 : (q' : Λ) → (s : Turing.TM0.Stmt Γ) → motive (some (q', s))) (q' : Λ) (s : Turing.TM0.Stmt Γ),
  x = some (q', s) →
    (match x with
      | none => h_1 ()
      | some (q', s) => h_2 q' s) ≍
      h_2 q' s
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  (HomologicalComplex.homotopyCofiber φ).X i = HomologicalComplex.homotopyCofiber.X φ i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_diff_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.coe_copy : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)) (f' : X → Y)
  (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObj.add_mul : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (R : C) [self : CategoryTheory.RingObj R],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add R)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.fst R R) R)
          CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.snd R R) R)
          CategoryTheory.MonObj.mul))
      CategoryTheory.AddMonObj.add
-- Mathlib.Combinatorics.Hall.Finite
HallMarriageTheorem.hall_cond_of_compl : ∀ {α : Type v} [inst : DecidableEq α] {ι : Type u} {t : ι → Finset α} {s : Finset ι},
  s.card = (s.biUnion t).card →
    (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) →
      ∀ (s' : Finset ↑(↑s)ᶜ), s'.card ≤ (s'.biUnion fun x' => t ↑x' \ s.biUnion t).card
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.projFn.sizeOf_spec : ∀ (baseStructName structName fieldName : Lean.Name) (levels : List Lean.Level),
  sizeOf (Lean.Elab.Term.LValResolution.projFn baseStructName structName fieldName levels) =
    1 + sizeOf baseStructName + sizeOf structName + sizeOf fieldName + sizeOf levels
-- Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
/-- If `f` is a bilinear map taking values in the space of alternating maps,
then evaluation of the twice uncurried `f` on a tuple of vectors `v`
can be represented as a sum of

$$
f(v_i, v_j; v_0, \dots, \hat{v_i}, \dots, \hat{v_j}-) -
f(v_j, v_i; v_0, \dots, \hat{v_i}, \dots, \hat{v_j}-)
$$

over all `(i j : Fin (n + 2))`, `i < j`, taken with appropriate signs.
Here $\hat{v_i}$ and $\hat{v_j}$ mean that these vectors are removed from the tuple.

We use pairs of `i j : Fin (n + 1)`, `i ≤ j`,
to encode pairs `(i.castSucc : Fin (n + 2), j.succ : Fin (n + 2))`,
so the power of `-1` is off by one compared to the informal texts.

In particular, if `f` is symmetric in the first two arguments,
then the resulting alternating map is zero,
see `alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric` below.
 -/
AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ} (f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v : Fin (n + 2) → M),
  (AlternatingMap.alternatizeUncurryFin (AlternatingMap.alternatizeUncurryFinLM ∘ₗ f)) v =
    ∑ i,
      ∑ j ≥ i,
        (-1) ^ (↑i + ↑j) •
          (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
            ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.instHasIsosQcPrecoverage : AlgebraicGeometry.Scheme.qcPrecoverage.HasIsos
-- Init.Classical
/-- Given that there exists an element satisfying `p`, returns one such element.

This is a straightforward consequence of, and equivalent to, `Classical.choice`.

See also `choose_spec`, which asserts that the returned value has property `p`.
 -/
Classical.choose : {α : Sort u} → {p : α → Prop} → (∃ x, p x) → α
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.Score.mk : Int16 → Lean.FuzzyMatching.Score✝
-- Std.Data.DTreeMap.Raw.Slice
Std.DTreeMap.Raw.toList_roc : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.toList_roc._auto_1)
  [Std.TransCmp cmp] {t : Std.DTreeMap.Raw α β cmp},
  t.WF →
    ∀ {lowerBound upperBound : α},
      Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
        List.filter (fun e => decide ((cmp e.fst lowerBound).isGT = true ∧ (cmp e.fst upperBound).isLE = true)) t.toList
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_comp_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : B × C} (f : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)) (g : (Y.1 ⟶ Z.1) × (Y.2 ⟶ Z.2)),
  (CategoryTheory.CategoryStruct.comp f g).1 = CategoryTheory.CategoryStruct.comp f.1 g.1
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (motive :
                (l_1 : Std.DTreeMap.Internal.Impl α β) →
                  l_1.Balanced →
                    Std.DTreeMap.Internal.Impl.BalanceLPrecond l_1.size
                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
                      Sort u_3) →
              (l_1 : Std.DTreeMap.Internal.Impl α β) →
                (hlb : l_1.Balanced) →
                  (hlr :
                      Std.DTreeMap.Internal.Impl.BalanceLPrecond l_1.size
                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                    ((hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                        (hlr :
                            Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
                              (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                          motive Std.DTreeMap.Internal.Impl.leaf hlb hlr) →
                      ((ls : ℕ) →
                          (lk : α) →
                            (lv : β lk) →
                              (ll lr : Std.DTreeMap.Internal.Impl α β) →
                                (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
                                  (hlr :
                                      Std.DTreeMap.Internal.Impl.BalanceLPrecond
                                        (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                                    motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr) →
                        motive l_1 hlb hlr