mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.succ_eval : Turing.ToPartrec.Code.succ.eval = fun v => pure [v.headI.succ]
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- Given a functor `F : Jᵒᵖ ⥤ Type v` where `J` is a well-ordered type,
this is a constructor for `F.WellOrderInductionData` which does not take
data as inputs but proofs of the existence of certain elements.  -/
CategoryTheory.Functor.WellOrderInductionData.ofExists : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        (∀ (j : J),
            ¬IsMax j →
              Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) →
          (∀ (j : J),
              Order.IsSuccLimit j →
                ∀ (x : ↑(⋯.functor.op.comp F).sections),
                  ∃ y,
                    ∀ (i : J) (hi : i < j),
                      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) y =
                        ↑x (Opposite.op ⟨i, hi⟩)) →
            F.WellOrderInductionData
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The internal hom out of the unit is naturally isomorphic to the identity functor.  -/
CategoryTheory.MonoidalClosed.unitNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] →
        CategoryTheory.Functor.id C ≅ CategoryTheory.ihom (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDerivWithin_fun_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {i : ℕ},
  iteratedFDerivWithin 𝕜 i (fun x => 0) s = 0
-- Mathlib.RingTheory.Idempotents
Ideal.mem_map_span_singleton_iff_of_isIdempotentElem : ∀ {R : Type u_1} [inst : CommRing R] {e r : R},
  IsIdempotentElem e →
    ∀ {I : Ideal R},
      (Ideal.Quotient.mk (Ideal.span {e})) r ∈ Ideal.map (Ideal.Quotient.mk (Ideal.span {e})) I ↔ (1 - e) * r ∈ I
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.addSubmonoid_smul_sup : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M : AddSubmonoid R} {N P : AddSubmonoid A}, M • (N ⊔ P) = M • N ⊔ M • P
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.isFiniteMeasure_restrict_Ioo : ∀ (x y : ℝ), MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Set.Ioo x y))
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xPrevIsoSelf_comp_dTo : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {j : ι}
  (h : ¬c.Rel (c.prev j) j), CategoryTheory.CategoryStruct.comp (C.xPrevIsoSelf h).inv (C.dTo j) = 0
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.instNonemptyUniformizer : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] (v : Valuation K Γ)
  [inst_2 : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup]
  [inst_3 : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup], Nonempty v.Uniformizer
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ Std.DTreeMap.Internal.Impl.insertIfNew! k v t → compare k a ≠ Ordering.eq → a ∈ t
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.comap_injective : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)),
  Function.Surjective f.toFun → Function.Injective (LocallyConstant.comap f)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_distribMulActionHom_mk : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A →ₛₙₐ[φ] B) (h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x)
  (h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : A),
      { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
        { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
          { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y),
  ↑{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } =
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }
-- Init.Data.SInt.Lemmas
Int64.toInt_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt = (↑n).bmod Int64.size
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instBot : {Ω : Type u_1} → {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → Bot (MeasureTheory.Filtration ι m)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.mk.sizeOf_spec : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : SizeOf J]
  (W : CategoryTheory.MorphismProperty J) (P : CategoryTheory.ObjectProperty J)
  (src : ∀ {i j : J} {f : i ⟶ j}, W f → P i) (tgt : ∀ {i j : J} {f : i ⟶ j}, W f → P j) (hW : W.HasCardinalLT κ)
  (hP : P.HasCardinalLT κ),
  sizeOf { W := W, P := P, src := src, tgt := tgt, hW := hW, hP := hP } = 1 + sizeOf hW + sizeOf hP
-- Mathlib.Data.Vector.Snoc
List.Vector.mapAccumr_snoc : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} {n : ℕ} {x : α} (xs : List.Vector α n) {f : α → σ → σ × β} {s : σ},
  List.Vector.mapAccumr f (xs.snoc x) s =
    have q := f x s;
    have r := List.Vector.mapAccumr f xs q.1;
    (r.1, r.2.snoc q.2)
-- Init.Data.Option.Lemmas
Option.isNone_eq_false_iff : ∀ {α : Type u_1} {a : Option α}, a.isNone = false ↔ a.isSome = true
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.Cover.ofQuasiCompactCover_toPreZeroHypercover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
  [qc : AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover],
  𝒰.ofQuasiCompactCover.toPreZeroHypercover = 𝒰.toPreZeroHypercover
-- Init.System.Promise
_private.Init.System.Promise.0.IO.Promise.mk : {α : Type} → IO.PromisePointed✝.type → Nonempty α → IO.Promise α
-- Mathlib.ModelTheory.LanguageMap
/-- The type of functions for a language consisting only of constant symbols.  -/
FirstOrder.Language.constantsOnFunc : Type u' → ℕ → Type u'
-- Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj : ∀ (b : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ),
  CommRingCat.moduleCatRestrictScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑(Opposite.unop b.as))
-- Mathlib.Order.Filter.Pointwise
Filter.top_mul_of_one_le : ∀ {α : Type u_2} [inst : Monoid α] {f : Filter α}, 1 ≤ f → ⊤ * f = ⊤
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.val_mk : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x : L} (hx : x ∈ S), S.val ⟨x, hx⟩ = x
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_im_pos : ∀ (self : UpperHalfPlane), 0 < (↑self).im
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
tendsto_rpow_neg_nhdsGT_zero : ∀ {y : ℝ}, y < 0 → Filter.Tendsto (fun x => x ^ y) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.integrate_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A)
  [hμA : μA.IsHaarMeasure] [inst_11 : NormedSpace ℝ E] [inst_12 : IsTopologicalGroup C]
  [inst_13 : LocallyCompactSpace B] [inst_14 : MeasurableSpace C] [inst_15 : BorelSpace C]
  (μC : MeasureTheory.Measure C) [hμC : μC.IsHaarMeasure] (f : CompactlySupportedContinuousMap B E),
  (H.integrate μA μC) f = ∫ (c : C), ((H.pushforward μA) f) c ∂μC
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHomClass.instSemilinearMapClassOfNonUnitalAlgSemiHomClassToMonoidHomRingHom : ∀ {F : Type u_3} {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} {x : Semiring R} {x_1 : Semiring S}
  {φ : R →+* S} {x_2 : NonUnitalSemiring A} {x_3 : NonUnitalSemiring B} [inst : Module R A] [inst_1 : Module S B]
  [inst_2 : FunLike F A B] [NonUnitalAlgSemiHomClass F (↑φ) A B], SemilinearMapClass F φ A B
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.le_one : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) {x : M} [inst_5 : FiniteDimensional ℝ E], ↑f x ≤ 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.mk_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W)
  (inr : Z ⟶ W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr)
  (j : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app j =
    Option.casesOn j (CategoryTheory.CategoryStruct.comp f inl) fun j' =>
      CategoryTheory.Limits.WalkingPair.casesOn j' inl inr
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.determineSignatureHelp : Lean.Elab.InfoTree → Lean.Syntax → IO (Option Lean.Lsp.SignatureHelp)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Module.Basis.equivFunL.congr_simp : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E]
  [inst_5 : CompleteSpace 𝕜] {ι : Type u_1} [inst_6 : Finite ι] [inst_7 : T2Space E] (v v_1 : Module.Basis ι 𝕜 E),
  v = v_1 → v.equivFunL = v_1.equivFunL
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.get! : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → [Inhabited (β a)] → β a
-- Mathlib.Algebra.Module.ULift
ULift.module' : {R : Type u} →
  {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Module R (ULift.{u_1, v} M)
-- Aesop.Rule.Name
Aesop.ScopeName.instOrd : Ord Aesop.ScopeName
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.inc_congr : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β}, H ≤ G → e ∈ H.edgeSet → (H.Inc e x ↔ G.Inc e x)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.eqOnSource_refl : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e ≈ e
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.isClosed_iff_isUpper : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] {s : Set α},
  IsClosed s ↔ IsUpperSet s
-- Mathlib.RingTheory.Smooth.Fiber
_private.Mathlib.RingTheory.Smooth.Fiber.0.Algebra.«term𝓀[_]» : Lean.ParserDescr
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.updateTokenCache : String.Pos.Raw → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Order.KrullDimension
/-- For elements of finite height, `height` is strictly monotone.  -/
Order.height_strictMono : ∀ {α : Type u_1} [inst : Preorder α] {x y : α}, x < y → Order.height x < ⊤ → Order.height x < Order.height y
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalAlgebra.lift_comp_of : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → NonUnitalNonAssocSemiring (G i)] [inst_6 : (i : ι) → DistribMulAction R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : DistribMulAction R P] (g : (i : ι) → G i →ₙₐ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι},
  (DirectLimit.NonUnitalAlgebra.lift G f P g Hg).comp (DirectLimit.NonUnitalAlgebra.of G f i) = g i
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.hom_ext_iff : ∀ {M N : CommMonCat} {f g : M ⟶ N}, f = g ↔ CommMonCat.Hom.hom f = CommMonCat.Hom.hom g
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {P Q : CategoryTheory.Idempotents.Karoubi C} {f : P ⟶ Q}, f = 0 ↔ f.f = 0
-- Mathlib.Topology.Inseparable
/-- Lift a map `f : X → Y → α` such that `Inseparable a b → Inseparable c d → f a c = f b d` to a
map `SeparationQuotient X → SeparationQuotient Y → α`.  -/
SeparationQuotient.lift₂ : {X : Type u_1} →
  {Y : Type u_2} →
    {α : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          (f : X → Y → α) →
            (∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d) →
              SeparationQuotient X → SeparationQuotient Y → α
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.liftToInitial_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsInitial Z) {X Y : CategoryTheory.WithInitial C}
  (f : X ⟶ Y),
  (CategoryTheory.WithInitial.liftToInitial F hZ).map f =
    match X, Y, f with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, f => F.map (CategoryTheory.WithInitial.down f)
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a, x => hZ.to (F.obj a)
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, x => CategoryTheory.CategoryStruct.id Z
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.self_comp_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), ⇑e ∘ ⇑e.symm = id
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.fromNormalizedChainComplex_f_toNormalizedChainComplex_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ),
  CategoryTheory.CategoryStruct.comp ((X.fromNormalizedChainComplex R).f n) ((X.toNormalizedChainComplex R).f n) =
    CategoryTheory.CategoryStruct.id ((X.normalizedChainComplex R).X n)
-- Mathlib.Order.Bounds.Basic
IsLeast.lowerBounds_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLeast s a → lowerBounds s = Set.Iic a
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' fallback : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k' (Std.Internal.List.modifyKey k f l) fallback =
      if (k == k') = true then if Std.Internal.List.containsKey k l = true then k else fallback
      else Std.Internal.List.getKeyD k' l fallback
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.MonoidalCategory.curriedTensorPreFunctor_map_app_app : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory D]
  {F₁ F₂ : CategoryTheory.Functor C D} (f : F₁ ⟶ F₂) (X₁ X₂ : C),
  ((CategoryTheory.MonoidalCategory.curriedTensorPreFunctor.map f).app X₁).app X₂ =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (f.app X₁) (f.app X₂)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
/-- In a unital C⋆-algebra, if `0 ≤ a` and `0 ≤ b` and `a` and `b` are units, then `a⁻¹ ≤ b⁻¹`
if and only if `b ≤ a`.  -/
CStarAlgebra.inv_le_inv_iff : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : Aˣ},
  0 ≤ ↑a → 0 ≤ ↑b → (↑a⁻¹ ≤ ↑b⁻¹ ↔ ↑b ≤ ↑a)
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balLeft.fun_cases_unfolding : ∀ {α : Type u_1} (v : α) (motive : RBTree.RBNode α → RBTree.RBNode α → RBTree.RBNode α → Prop),
  (∀ (r a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
      motive (RBTree.RBNode.node RBTree.RBColor.red a x b) r
        (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a x b) v r)) →
    (∀ (l : RBTree.RBNode α),
        (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
            l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
          ∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α),
            motive l (RBTree.RBNode.node RBTree.RBColor.black a y b)
              (l.balance2 v (RBTree.RBNode.node RBTree.RBColor.red a y b))) →
      (∀ (l : RBTree.RBNode α),
          (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
              l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
            ∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α) (c : RBTree.RBNode α),
              motive l (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c)
                (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black l v a) y
                  (b.balance2 z c.setRed))) →
        (∀ (l : RBTree.RBNode α),
            (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
              ∀ (r : RBTree.RBNode α),
                (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α),
                    r = RBTree.RBNode.node RBTree.RBColor.black a y b → False) →
                  (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α) (c : RBTree.RBNode α),
                      r = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c →
                        False) →
                    motive l r (RBTree.RBNode.node RBTree.RBColor.red l v r)) →
          ∀ (l r : RBTree.RBNode α), motive l r (l.balLeft v r)
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, returning `none` if the map is empty.
 -/
Std.TreeMap.maxKey? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Option α
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_gen.congr_simp : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F F_1 : Polynomial R} (e_F : F = F_1) {a a_1 : ℤ_[p]} (e_a : a = a_1)
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (n n_1 : ℕ),
  n = n_1 → newton_seq_gen✝ hnorm n = newton_seq_gen✝ ⋯ n_1
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_coeff_cert.eq_1 : ∀ (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.norm_eq_coeff_cert lhs rhs p k = ((lhs.sub rhs).norm.beq' (p.mul_k k)).and' (Int.blt' 0 k)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.aeval_minpolyGen : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S),
  (Polynomial.aeval pb.gen) pb.minpolyGen = 0
-- Mathlib.Tactic.FunProp.ToBatteries
/-- Apply the given arguments to `f`, beta-reducing if `f` is a lambda expression. This variant
does beta-reduction through let bindings without inlining them.

Example
```
beta' (fun x => let y := x * x; fun z => x + y + z) #[a,b]
==>
let y := a * a; a + y + b
```
 -/
Mathlib.Meta.FunProp.betaThroughLet : Lean.Expr → Array Lean.Expr → Lean.Expr
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone decreasing collection of continuous functions on a
compact set `s` converging pointwise to a continuous `f`, then `F n` converges uniformly to `f`.  -/
Antitone.tendstoUniformlyOn_of_forall_tendsto : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G} {s : Set α},
  IsCompact s →
    (∀ (i : ι), ContinuousOn (F i) s) →
      (∀ x ∈ s, Antitone fun x_1 => F x_1 x) →
        ContinuousOn f s →
          (∀ x ∈ s, Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) →
            TendstoUniformlyOn F f Filter.atTop s
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.functorHom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {X : C} {x y : (F.functorHom G).obj X},
  (∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f) → x = y
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Sub-add-sub version.  -/
Finset.ruzsa_triangle_inequality_sub_add_sub : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] (A B C : Finset G),
  (A - C).card * B.card ≤ (A + B).card * (B - C).card
-- Std.Http.Internal.IndexMultiMap
/-- A structure for managing ordered key-value pairs where each key can have multiple values.
 -/
Std.Internal.IndexMultiMap : (α : Type u) → Type v → [BEq α] → [Hashable α] → Type (max u v)
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- The geometric series converges if the constant term is zero.  -/
MvPowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R] {f : MvPowerSeries σ R},
  MvPowerSeries.constantCoeff f = 0 → Summable fun x => f ^ x
-- Mathlib.Algebra.Quandle
/-- Action of a Shelf  -/
Quandles.«term_◃_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentials.hom₁_single : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ) (r : σ),
  ((Algebra.Presentation.differentials.hom₁ pres) fun₀ | r => 1) = Algebra.Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_eq_singleton : ∀ {m n : ℕ}, n = m + 1 → (m...n).toArray = #[m]
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn : ∀ (p : ℝ),
  AkraBazziRecurrence.GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) x‖
-- Mathlib.Algebra.Order.Ring.Cast
Int.cast_mono : ∀ {R : Type u_1} [inst : AddCommGroupWithOne R] [inst_1 : PartialOrder R] [AddLeftMono R] [ZeroLEOneClass R],
  Monotone Int.cast
-- Mathlib.RingTheory.SimpleRing.Basic
RingHom.injective : ∀ {R : Type u_2} {S : Type u_3} [inst : NonAssocRing R] [IsSimpleRing R] [inst_2 : NonAssocSemiring S] [Nontrivial S]
  (f : R →+* S), Function.Injective ⇑f