mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciSup_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] [inst_1 : Preorder β] {f : β → α}
  (a : β), Monotone f → ⨆ x, f ↑x = f a
-- Batteries.Data.Array.Scan
Array.size_scanr : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} (init : β) (as : Array α), (Array.scanr f init as).size = as.size + 1
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.coe_vadd : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G β] (g : G) (f : α ↪ β),
  ⇑(g +ᵥ f) = g +ᵥ ⇑f
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.OplaxLeftLinear C] (c c' : C) (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
          (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c' d))
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).inv) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv)
      (CategoryTheory.Functor.OplaxLeftLinear.δₗ F (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supportedEquivFinsupp_symm_single : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set α) (i : ↑s) (a : M), ↑((Finsupp.supportedEquivFinsupp s).symm fun₀ | i => a) = fun₀ | ↑i => a
-- Mathlib.Order.Filter.Extr
/-- `IsExtrFilter f l a` means `IsMinFilter f l a` or `IsMaxFilter f l a`  -/
IsExtrFilter : {α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Filter α → α → Prop
-- Mathlib.Topology.Category.Profinite.Basic
/-- An explicit limit cone for a functor `F : J ⥤ Profinite`, defined in terms of
`CompHaus.limitCone`, which is defined in terms of `TopCat.limitCone`.  -/
Profinite.limitCone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → (F : CategoryTheory.Functor J Profinite) → CategoryTheory.Limits.Cone F
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.trans_toEquiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] (ab : α ≃ᵐ β) (bc : β ≃ᵐ γ), (ab.trans bc).toEquiv = ab.trans bc.toEquiv
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_apply : ∀ {α : Type u_1} {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] (v w : V) [inst_1 : Zero α]
  [inst_2 : One α], SimpleGraph.adjMatrix α G v w = if G.Adj v w then 1 else 0
-- Lean.Meta.Basic
Lean.Meta.SynthInstanceCacheKey.mk.injEq : ∀ (localInsts : Lean.LocalInstances) (type : Lean.Expr) (synthPendingDepth : ℕ) (localInsts_1 : Lean.LocalInstances)
  (type_1 : Lean.Expr) (synthPendingDepth_1 : ℕ),
  ({ localInsts := localInsts, type := type, synthPendingDepth := synthPendingDepth } =
      { localInsts := localInsts_1, type := type_1, synthPendingDepth := synthPendingDepth_1 }) =
    (localInsts = localInsts_1 ∧ type = type_1 ∧ synthPendingDepth = synthPendingDepth_1)
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S)
  [inst_3 : p.IsPrime] [IsArtinianRing R] [Algebra.EssFiniteType R S] [Algebra.QuasiFiniteAt R p],
  ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst_3 }}
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The image of a pullback cone by a functor.  -/
CategoryTheory.Limits.PullbackCone.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X Y Z : C} →
          {f : X ⟶ Z} →
            {g : Y ⟶ Z} →
              CategoryTheory.Limits.PullbackCone f g →
                (G : CategoryTheory.Functor C D) → CategoryTheory.Limits.PullbackCone (G.map f) (G.map g)
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instSDiffOfBEqOfHashable : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → SDiff (Std.HashMap.Raw α β)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addSimproc.injEq : ∀ («simproc» : Lean.Name) (post : Bool) (simproc_1 : Lean.Name) (post_1 : Bool),
  (Lean.Elab.Tactic.ElabSimpArgResult.addSimproc «simproc» post =
      Lean.Elab.Tactic.ElabSimpArgResult.addSimproc simproc_1 post_1) =
    («simproc» = simproc_1 ∧ post = post_1)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Basis sets for the uniformity of `𝔖`-convergence: for `S : Set α` and `V : Set (β × β)`,
`gen 𝔖 S V` is the set of pairs `(f, g)` of functions `α →ᵤ[𝔖] β` such that
`∀ x ∈ S, (f x, g x) ∈ V`. Note that the family `𝔖 : Set (Set α)` is only used to specify which
type alias of `α → β` to use here.  -/
UniformOnFun.gen : {α : Type u_1} →
  {β : Type u_2} → (𝔖 : Set (Set α)) → Set α → Set (β × β) → Set (UniformOnFun α β 𝔖 × UniformOnFun α β 𝔖)
-- Mathlib.Order.Lattice
Antitone.le_map_inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeSup β] {f : α → β},
  Antitone f → ∀ (x y : α), f x ⊔ f y ≤ f (x ⊓ y)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {a : α}, a +ᵥ Set.univ = Set.univ
-- Init.Data.List.MinMaxOn
List.minOn?_eq_if : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α}, List.minOn? f xs = if h : xs ≠ [] then some (List.minOn f xs h) else none
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.namespace : Lean.Lsp.SymbolKind
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsNonZero → ∀ (n : ℤ), LieAlgebra.rootSpace H (-n • ⇑α + ⇑β) ≠ ⊥ → n ≤ ↑(LieModule.chainBotCoeff (⇑α) β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_le_maxKey?_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.maxKey? = some km → (Std.DTreeMap.Internal.Impl.insert! k v t).maxKey?.get ⋯ = kmi → (compare km kmi).isLE = true
-- Mathlib.Algebra.Group.Prod
Prod.addCommute_iff : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] {x y : M × N},
  AddCommute x y ↔ AddCommute x.1 y.1 ∧ AddCommute x.2 y.2
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wp_consequence : ∀ {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog)
  (post post' : Value → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel post post' →
    Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x post epost) (Std.Internal.Do.wp x post' epost)
-- Mathlib.Order.Bounds.Image
AntitoneOn.mem_lowerBounds_image_self : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {t : Set α} {a : α},
  AntitoneOn f t → a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.mapIso_inv_π_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) {Z : C} (h : f b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) (CategoryTheory.CategoryStruct.comp (p b).inv h)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.distortion_le_iff : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [inst : Fintype ι] {c : NNReal},
  π.distortion ≤ c ↔ ∀ J ∈ π, J.distortion ≤ c
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_empty : ∀ {α : Type u_1} (M : Matroid α), M.closure ∅ = M.loops
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- This is a more convenient formulation to show that a `PullbackCone` constructed using
`PullbackCone.mk` is a weak limit cone.
 -/
CategoryTheory.Limits.PullbackCone.IsWeakLimit.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {W : C} →
            {fst : W ⟶ X} →
              {snd : W ⟶ Y} →
                (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g) →
                  (lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt ⟶ W) →
                    (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                        CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) →
                      (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                          CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) →
                        CategoryTheory.Limits.IsWeakLimit (CategoryTheory.Limits.PullbackCone.mk fst snd eq)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.presheafIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ ℱ' : CategoryTheory.Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj),
  (CategoryTheory.Functor.IsCoverDense.presheafIso i).inv =
    CategoryTheory.inv (CategoryTheory.Functor.IsCoverDense.sheafHom i.hom)
-- Lean.LocalContext
Lean.LocalDeclKind.implDetail.sizeOf_spec : sizeOf Lean.LocalDeclKind.implDetail = 1
-- Init.RCases
/-- The `rintro` tactic is a combination of the `intros` tactic with `rcases` to
allow for destructuring patterns while introducing variables. See `rcases` for
a description of supported patterns. For example, `rintro (a | ⟨b, c⟩) ⟨d, e⟩`
will introduce two variables, and then do case splits on both of them producing
two subgoals, one with variables `a d e` and the other with `b c d e`.

`rintro`, unlike `rcases`, also supports the form `(x y : ty)` for introducing
and type-ascripting multiple variables at once, similar to binders.
 -/
Lean.Parser.Tactic.rintro : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.homEquiv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x₀ x₁ x₂ : CategoryTheory.ComposableArrows C 0}
  {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂} {e₀₂ : SSet.Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.nerve.homEquiv e₀₁) (CategoryTheory.nerve.homEquiv e₁₂) =
    CategoryTheory.nerve.homEquiv e₀₂
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.Sheaf.IsConstant.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {F : CategoryTheory.Sheaf J D}, (CategoryTheory.constantSheaf J D).essImage F → CategoryTheory.Sheaf.IsConstant J F
-- Lean.Elab.Tactic.Grind.Basic
/-- Like `throwErrorAt`, but, if recovery is enabled, logs the error instead.
 -/
Lean.Elab.Tactic.Grind.throwOrLogErrorAt : Lean.Syntax → Lean.MessageData → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
/-- An equivalence of categories lifts to an equivalence of their commutative group objects.  -/
CategoryTheory.Equivalence.mapCommGrp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.CartesianMonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (e : C ≌ D) →
                  [e.functor.Braided] → [e.inverse.Braided] → CategoryTheory.CommGrp C ≌ CategoryTheory.CommGrp D
-- Lean.Meta.Tactic.SolveByElim
/-- A `MetaM` analogue of the `apply_rules` user tactic.

We pass the lemmas as `TermElabM Expr` rather than just `Expr`,
so they can be generated fresh for each application, to avoid stuck metavariables.

By default it uses all local hypotheses, but you can disable this with `only := true`.
If you need to remove particular local hypotheses, call `solveByElim` directly.
 -/
Lean.MVarId.applyRules : Lean.Meta.SolveByElim.SolveByElimConfig →
  List (Lean.Elab.TermElabM Lean.Expr) → optParam Bool false → Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Init.Data.UInt.Bitwise
UInt32.not_inj : ∀ {a b : UInt32}, ~~~a = ~~~b ↔ a = b
-- Mathlib.Data.Complex.Basic
Complex.instIsAddTorsionFree : IsAddTorsionFree ℂ
-- Mathlib.Control.ULift
ULift.map_up : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α), ULift.map f { down := a } = { down := f a }
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonneg_mul_lem : ∀ {d x y : ℕ} {a : ℤ√↑d}, a.Nonneg → ({ re := ↑x, im := ↑y } * a).Nonneg
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instModuleHom : {k : Type u} →
  {G : Type v} → [inst : CommSemiring k] → [inst_1 : Monoid G] → {M N : Rep.{u_1, u, v} k G} → Module k (M ⟶ N)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameParams.mk.injEq : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (newName : String)
  (toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams) (newName_1 : String),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams, newName := newName } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1, newName := newName_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1 ∧ newName = newName_1)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonUnitalSemiringOfNonUnitalRingHomClass : {ι : 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 ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalSemiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                      NonUnitalSemiring (DirectLimit G f)
-- Init.Meta.Defs
Lean.version.specialDesc : String
-- Init.Prelude
/-- Converts a `List α` into an `Array α`.

 `O(|xs|)`. At runtime, this operation is implemented by `List.toArrayImpl` and takes time linear in
the length of the list. `List.toArray` should be used instead of `Array.mk`.

Examples:
 * `[1, 2, 3].toArray = #[1, 2, 3]`
 * `["monday", "wednesday", friday"].toArray = #["monday", "wednesday", friday"].`
 -/
List.toArray : {α : Type u_1} → List α → Array α
-- Lean.Server.GoTo
Lean.Server.getInstanceProjectionArg? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Lean.Data.Json.FromToJson.Basic
/-- Parses a JSON-encoded `structure` or `inductive` constructor, assuming the tag has already been
checked and `nFields` is nonzero. Used mostly by `deriving FromJson`.
 -/
Lean.Json.parseCtorFields : Lean.Json → String → ℕ → Option (Array Lean.Name) → Except String (Array Lean.Json)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.isStrictlyPositive_iff_exists_isStrictlyPositive_and_eq_mul_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A}, IsStrictlyPositive a ↔ ∃ b, IsStrictlyPositive b ∧ a = b * b
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} →
              (generators : M.GeneratingSections) →
                (CategoryTheory.Limits.kernel generators.π).GeneratingSections → M.Presentation
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.IsSubnormal.subgroupOf : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsSubnormal → (H.subgroupOf K).IsSubnormal
-- Mathlib.Order.RelClasses
/-- Creates data, given a way to generate a value from all that compare as lesser. See also
`WellFoundedLT.fix_eq`.  -/
WellFoundedLT.fix : {α : Type u} →
  [inst : LT α] →
    [WellFoundedLT α] →
      {motive : α → Sort u_1} → ((x : α) → ((y : α) → y < x → motive y) → motive x) → (x : α) → motive x
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.vadd_closedEBall`. -/
EMetric.vadd_closedBall : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal), c +ᵥ Metric.closedEBall x r = Metric.closedEBall (c +ᵥ x) r
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandlerKind : Type
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.LeapSecond.mk.sizeOf_spec : ∀ (transitionTime correction : ℤ),
  sizeOf { transitionTime := transitionTime, correction := correction } = 1 + sizeOf transitionTime + sizeOf correction
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_map_eq : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : SeminormedAddCommGroup β] (A : Matrix m n α) (f : α → β),
  (∀ (a : α), ‖f a‖₊ = ‖a‖₊) → ‖A.map f‖₊ = ‖A‖₊
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.IsLiesOverAlgebra.mk : ∀ {A : Type u_4} {B : Type u_5} [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B] {p : Ideal A}
  [inst_3 : p.IsPrime] {P : Ideal B} [inst_4 : P.IsPrime] [inst_5 : P.LiesOver p]
  [inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime P)],
  algebraMap (Localization.AtPrime p) (Localization.AtPrime P) = Localization.localRingHom p P (algebraMap A B) ⋯ →
    Localization.AtPrime.IsLiesOverAlgebra p P
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.replaceVertex_self : ∀ {V : Type u_1} (G : SimpleGraph V) (s : V) [inst : DecidableEq V], G.replaceVertex s s = G
-- Mathlib.Data.ENat.Basic
ENat.lift_zero : ENat.lift 0 ⋯ = 0
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_abs_iff : ∀ {x : ℝ*}, |x|.Infinite ↔ x.Infinite
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Collinear points are coplanar.  -/
Collinear.coplanar : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, Collinear k s → Coplanar k s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrpObjRepresentableBy.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.AddGrpObj G],
  CategoryTheory.yonedaAddGrpObjRepresentableBy G =
    CategoryTheory.Functor.representableByEquiv.symm (CategoryTheory.Iso.refl (CategoryTheory.yoneda.obj G))
-- Mathlib.RingTheory.Polynomial.Basic
/-- The push-forward of an ideal `I` of `R` to `R[X]` via inclusion
is exactly the set of polynomials whose coefficients are in `I`  -/
Ideal.mem_map_C_iff : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} {f : Polynomial R},
  f ∈ Ideal.map Polynomial.C I ↔ ∀ (n : ℕ), f.coeff n ∈ I
-- Mathlib.Data.List.TFAE
List.tfae_singleton : ∀ (p : Prop), [p].TFAE
-- Mathlib.Data.Nat.Cast.Order.Field
Nat.inv_pos_of_nat : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {n : ℕ}, 0 < (↑n + 1)⁻¹
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.preservesFiniteLimits_iff : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_3, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_5, u_3} C] (F : CategoryTheory.Functor J C),
  CategoryTheory.ObjectProperty.preservesFiniteLimits F ↔ CategoryTheory.Limits.PreservesFiniteLimits F
-- Mathlib.GroupTheory.Nilpotent
/-- The preimage of a nilpotent group is nilpotent if the kernel of the homomorphism is contained
in the center.  -/
Subgroup.isNilpotent_of_ker_le_center : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G →* H),
  f.ker ≤ Subgroup.center G → ∀ [Group.IsNilpotent H], Group.IsNilpotent G
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.comp_apply : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} {N : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid N]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R N] {Q₁ : QuadraticMap R M₁ N}
  {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) (x : M₁), (g.comp f) x = g (f x)
-- Init.Data.List.Zip
List.head?_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ},
  (List.zipWithAll f as bs).head? =
    match as.head?, bs.head? with
    | none, none => none
    | a?, b? => some (f a? b?)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.gc_map_comap : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] {f : L →ₗ⁅R⁆ L₂},
  GaloisConnection (LieSubalgebra.map f) (LieSubalgebra.comap f)
-- Mathlib.Order.Filter.CountableInter
CountableInterFilter.mk : ∀ {α : Type u_2} {l : Filter α},
  (∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l) → CountableInterFilter l
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.iSup.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : Finite α] (f : α → L.Formula β),
  FirstOrder.Language.Formula.iSup f = FirstOrder.Language.BoundedFormula.iSup f
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.leRec.match_1.eq_1 : ∀ {n : ℕ} (motive : (x : ℕ) → n ≤ x → Sort u_1) (H : n ≤ 0) (h_1 : (H : n ≤ 0) → motive 0 H)
  (h_2 : (m : ℕ) → (H : n ≤ m + 1) → motive m.succ H),
  (match 0, H with
    | 0, H => h_1 H
    | m.succ, H => h_2 m H) =
    h_1 H